# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-domains base
base-nnp base Naked pointers prohibited in the OCaml heap
base-threads base
base-unix base
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.18.0 The Coq Proof Assistant
coq-core 8.18.0 The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib 8.18.0 The Coq Proof Assistant -- Standard Library
coqide-server 8.18.0 The Coq Proof Assistant, XML protocol server
dune 3.13.0 Fast, portable, and opinionated build system
ocaml 5.0.0 The OCaml compiler (virtual package)
ocaml-base-compiler 5.0.0 Official release 5.0.0
ocaml-config 3 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "palmskog@gmail.com"
homepage: "https://github.com/coq-community/coqtail-math"
dev-repo: "git+https://github.com/coq-community/coqtail-math.git"
bug-reports: "https://github.com/coq-community/coqtail-math/issues"
license: "LGPL-3.0-only"
synopsis: "Library of mathematical theorems and tools proved inside the Coq"
description: """
Coqtail is a library of mathematical theorems and tools proved inside
the Coq proof assistant. Results range mostly from arithmetic to real
and complex analysis."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {>= "8.11" & < "8.19"}
]
tags: [
"category:Mathematics/Real Calculus and Topology"
"keyword:real analysis"
"keyword:complex analysis"
"logpath:Coqtail"
"date:2023-11-23"
]
authors: [
"Guillaume Allais"
"Sylvain Dailler"
"Hugo Férée"
"Jean-Marie Madiot"
"Pierre-Marie Pédrot"
"Amaury Pouly"
]
url {
src: "https://github.com/coq-community/coqtail-math/archive/8.18.tar.gz"
checksum: "sha512=e0dd64426ac5ba25603ed57d3908b533c9c674aba453178851ae14f95dac81bab56eb16a9302b7a29079596057353fed773b99076449d3cd132f2e0ef6c6c1f1"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-coqtail.8.18 coq.8.18.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; timeout 4h opam install -y --deps-only coq-coqtail.8.18 coq.8.18.0opam list; echo; timeout 4h opam install -y -v coq-coqtail.8.18 coq.8.18.0Total: 20 M
../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Hopital.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rzeta2.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Lagrange_four_square.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_diff.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rzeta2.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Croot_n.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_cv_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Hopital.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Wallis.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rel_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_deriv.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cprop_base.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/CFsequence_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Ndiv.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_derivability.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_base_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cprop_base.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Croot_n.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_cv_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Ndiv.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rtactic.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Wallis.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_cv_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rel_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RFsequence_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/MillerRabin.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_diff.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRfunctions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRfunctions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis5.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Lagrange_four_square.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cexp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_prop.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_usual.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_deriv.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ratan.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Csequence_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/CFsequence_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_base_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_sums_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_usual_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cexp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_usual_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Hopital.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Znumfacts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_usual.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_definition.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_derivability.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Riemann_integrable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_instance.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis5.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_sums_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def_simpl.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ratan.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_cv_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Reirr.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RStirling.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rinterval.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/MillerRabin.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cderiv.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cbase.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpow_plus.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RFsequence_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Natsets.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_cv_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rinterval.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_quote.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cmet.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpow_plus.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Csequence_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RTaylor.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/Evect.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Modulo.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Hierarchy/Commutative_ring_binomial.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Reirr.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Riemann_integrable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_taylor.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RStirling.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_radius_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cnorm.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics_reflection.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cmet.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_cv_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cderiv.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rtactic.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_base_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRIneq.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cnorm.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def_simpl.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpow_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_radius_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Logic/Runcountable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_base_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_monotonicity.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rtrigo_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Logic/Runcountable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Logic/Rmarkov.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRIneq.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpow_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpolar.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_RiemannInt.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_subsequence.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_RiemannInt.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Ztools.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Hierarchy/Commutative_ring_binomial.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Triangular.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_base_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Logic/Rmarkov.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Cauchy_lipschitz.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Zlittle_fermat.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_monotonicity.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_extend.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_definition.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_def.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_continuity.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cfunctions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rzeta2.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_taylor.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RTaylor.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_usual.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_remainder_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_examples.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_basic_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nlittle_fermat.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_def.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RIVT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def_simpl.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_def.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_instance.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rtrigo_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_usual.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cseries_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nlittle_fermat.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rewrite_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nnewton.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_def.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_diff.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_def.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rextensionality.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Zprime.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_cont.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpow.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Finite_Calculus/Definitions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_ring.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_base_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/realisation_by_stdlib.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Ctacfield.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cbase.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_usual.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_cv_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_usual.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nbinomial.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nbinomial.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_pos_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/Evect.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Ndiv.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_MVT.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_bound_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/CFsequence.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_quote.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cdefinitions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Csequence_def.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyR_dist.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_prop.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_tactic.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cseries.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_def.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_deriv.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_subsequence.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/integrales.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RFsequence.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rel_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_def.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_base_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Zeqm.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Natsets.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_def.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Csequence.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyNNR.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics_reflection.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cprop_base.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_base_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_def.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nnewton.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_continuity.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nfinite_prod.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpolar.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nfinite_sum.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rewrite_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Cauchy_lipschitz.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_stdlib.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_derivability.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Zpow.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyINR.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Complex.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyReals.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbasic_fun.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbase.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Znumfacts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/Vectorial_Cauchy.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Wallis.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRfunctions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/MyNat.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nfinite_sum.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/CFsequence_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Ztools.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cseries_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis5.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_base_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cfunctions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Modulo.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def_simpl.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_cv_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_basic_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_usual.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Croot_n.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_def.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ratan.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RIVT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/integrales.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_remainder_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/MyZ.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nk_ind.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_extend.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Lagrange_four_square.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Ninductions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nk_ind.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Npow.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_def.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RFsequence_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_def.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_cont.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rtactic.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_usual_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/MillerRabin.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Zlittle_fermat.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/PI.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Riemann_integrable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_sums_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cexp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rinterval.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def_simpl.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_usual.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Csequence_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_MVT.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nfinite_prod.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rextensionality.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_usual.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nle.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_bound_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_monotonicity.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Ntools.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_usual.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cderiv.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_radius_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/realisation_by_stdlib.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nminus.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_def.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Reirr.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cmet.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_pos_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_def.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Functions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Triangular.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRIneq.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Finite_Calculus/Definitions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RTaylor.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RStirling.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_base_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cdefinitions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Natsets.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_quote.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_instance.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Monad.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cnorm.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_examples.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Zeqm.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Logic/Rmarkov.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Examples.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_cv_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Zpow.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cbase.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Logic/Runcountable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_RiemannInt.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Csequence_def.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_subsequence.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_base_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nbinomial.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpow.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics_reflection.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpow_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rtrigo_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Examples.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_taylor.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Functions.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Modulo.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Hierarchy/Commutative_ring_binomial.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Znumfacts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_definition.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_prop.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpow_plus.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Npow.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyR_dist.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_extend.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Zprime.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_continuity.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Monad.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/CFsequence.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nk_ind.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Ztools.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Monad/Option.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Monad/Option.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RFsequence.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/Vectorial_Cauchy.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RIVT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nlittle_fermat.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nfinite_sum.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rewrite_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpolar.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cfunctions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_def.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_ring.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_def.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_cont.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/PI.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cseries_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/Evect.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_def.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_basic_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nnewton.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_usual.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Choice_facts.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def_simpl.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_usual.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nfinite_prod.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_base_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Cauchy_lipschitz.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_def.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/MyNeq.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Ctacfield.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/MyNat.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_def.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Choice_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Triangular.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Zlittle_fermat.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_def.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_usual.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_remainder_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/realisation_by_stdlib.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_def.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_def.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_MVT.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cdefinitions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rextensionality.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_facts.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cseries.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Ninductions.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/InhabitedTactics.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_pos_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Npow.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/integrales.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_usual.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Csequence_def.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_ring.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpow.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_bound_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_tactic.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/CFsequence.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Zprime.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/RFsequence.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_tactic.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_examples.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Ctacfield.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Zpow.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Finite_Calculus/Definitions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Zeqm.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Tactics.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Examples.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Functions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_def.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_def.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_def.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_usual.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Monad.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_def.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Cseries.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/PI.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Monad/Option.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyR_dist.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nle.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Ntools.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/MyNat.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Complex.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/MyZ.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_def.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbasic_fun.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Ntools.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nminus.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbase.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyReals.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nle.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyNNR.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_stdlib.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/Vectorial_Cauchy.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Choice_facts.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyINR.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/MyNeq.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbasic_fun.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Ninductions.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/InhabitedTactics.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rpser.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/InhabitedTactics.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Complex.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_stdlib.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/MyZ.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyNNR.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyINR.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Rseries.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyReals.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbase.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Csequence.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Arith/Nminus.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/mytheories/MyNeq.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Tactics.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Reals/Tactics.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/Coqtail/Complex/Csequence.vopam remove -y coq-coqtail.8.18