# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-gmp 4 Virtual package relying on a GMP lib system installation coq 8.14.1 Formal proof management system dune 3.6.2 Fast, portable, and opinionated build system ocaml 4.08.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.08.1 Official release 4.08.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.5 A library manager for OCaml zarith 1.12 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.16~"} ] tags: [ "category:Mathematics/Real Calculus and Topology" "keyword:real analysis" "keyword:complex analysis" "logpath:Coqtail" "date:2021-11-02" ] 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.14.tar.gz" checksum: "sha512=ed7d54c4d42a01ae92db6c2116e503caace26462ccee46630a0256865440122ca044984ee249c30dbef78a7d83d6bda568873a1c579c6279dc1ed49a83812e31" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-coqtail.8.14 coq.8.14.1
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-coqtail.8.14 coq.8.14.1
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-coqtail.8.14 coq.8.14.1
Total: 20 M
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Hopital.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Lagrange_four_square.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rzeta2.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_diff.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rzeta2.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Croot_n.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_cv_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Hopital.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpser_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Wallis.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cprop_base.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rel_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_deriv.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/CFsequence_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Ndiv.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_derivability.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_base_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cprop_base.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Croot_n.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_cv_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Ndiv.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rtactic.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Wallis.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_cv_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rel_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RFsequence_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpser_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/MillerRabin.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_diff.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRfunctions.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRfunctions.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis5.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Lagrange_four_square.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cexp.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_usual.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_prop.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_deriv.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rintegral.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ratan.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Csequence_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_base_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/CFsequence_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_sums_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cexp.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_usual_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_usual_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Hopital.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Znumfacts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_instance.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_definition.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_usual.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis5.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_derivability.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rintegral.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Riemann_integrable.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_sums_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def_simpl.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ratan.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_cv_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Reirr.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RStirling.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rinterval.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/MillerRabin.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cbase.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cderiv.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpow_plus.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Natsets.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rinterval.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RFsequence_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cmet.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_cv_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_quote.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpow_plus.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Csequence_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RTaylor.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ediff/Evect.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Hierarchy/Commutative_ring_binomial.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Reirr.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Riemann_integrable.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Modulo.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_taylor.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RStirling.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_radius_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cnorm.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics_reflection.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cmet.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_cv_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cderiv.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rtactic.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpser_base_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRIneq.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cnorm.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def_simpl.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_radius_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpow_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Logic/Runcountable.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpser_base_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_monotonicity.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rtrigo_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRIneq.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Logic/Runcountable.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Logic/Rmarkov.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpow_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpolar.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_subsequence.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_RiemannInt.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_RiemannInt.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Hierarchy/Commutative_ring_binomial.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Ztools.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Triangular.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_base_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_monotonicity.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Logic/Rmarkov.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Cauchy_lipschitz.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Zlittle_fermat.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_definition.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_extend.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_def.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_continuity.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rzeta2.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cfunctions.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_taylor.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RTaylor.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_usual.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_remainder_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_basic_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_examples.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_def.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nlittle_fermat.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RIVT.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def_simpl.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_def.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_instance.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rtrigo_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nlittle_fermat.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_usual.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rewrite_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cseries_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nnewton.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_diff.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_def.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_def.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rextensionality.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_cont.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_ring.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpow.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Finite_Calculus/Definitions.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_base_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Zprime.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cbase.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ediff/realisation_by_stdlib.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_usual.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Ctacfield.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_cv_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nbinomial.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nbinomial.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_usual.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpser_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ediff/Evect.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Ndiv.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_pos_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_MVT.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_bound_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_quote.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/CFsequence.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cdefinitions.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Csequence_def.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyR_dist.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_prop.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_def.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_deriv.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_subsequence.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_tactic.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cseries.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ediff/integrales.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RFsequence.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rel_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_base_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpser_def.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Zeqm.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Natsets.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_def.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Csequence.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyNNR.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cprop_base.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_base_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_continuity.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics_reflection.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nfinite_prod.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nnewton.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpolar.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_def.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rewrite_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nfinite_sum.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Cauchy_lipschitz.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_derivability.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_stdlib.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Zpow.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Znumfacts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyINR.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Wallis.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Complex.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyReals.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbasic_fun.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRfunctions.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbase.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ediff/Vectorial_Cauchy.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/MyNat.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nfinite_sum.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/CFsequence_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Ztools.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cseries_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis5.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_base_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cfunctions.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def_simpl.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Modulo.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_cv_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_basic_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_usual.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Croot_n.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_def.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ratan.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RIVT.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ediff/integrales.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_remainder_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nk_ind.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_extend.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Lagrange_four_square.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/MyZ.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rintegral.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Ninductions.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nk_ind.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Npow.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_def.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RFsequence_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_cont.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rtactic.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_def.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_usual_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/MillerRabin.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Zlittle_fermat.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Riemann_integrable.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/PI.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_sums_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cexp.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rinterval.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def_simpl.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_usual.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Csequence_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_MVT.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nfinite_prod.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rextensionality.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_usual.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_bound_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_monotonicity.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nle.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cderiv.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Ntools.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_usual.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_radius_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ediff/realisation_by_stdlib.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Reirr.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_def.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nminus.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cmet.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_pos_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Functions.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Triangular.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRIneq.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_def.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Finite_Calculus/Definitions.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RTaylor.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RStirling.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpser_base_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cdefinitions.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Natsets.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_quote.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_instance.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Monad.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cnorm.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_examples.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Zeqm.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Logic/Rmarkov.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Examples.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_cv_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cbase.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Zpow.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Logic/Runcountable.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_RiemannInt.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Examples.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Csequence_def.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_subsequence.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_base_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nbinomial.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpow.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics_reflection.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Functions.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpow_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rtrigo_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_taylor.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Modulo.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Hierarchy/Commutative_ring_binomial.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Znumfacts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_definition.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_prop.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Monad.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpow_plus.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Npow.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_extend.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyR_dist.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Zprime.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_continuity.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Monad/Option.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/CFsequence.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nk_ind.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Ztools.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Monad/Option.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RFsequence.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ediff/Vectorial_Cauchy.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RIVT.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nlittle_fermat.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nfinite_sum.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rewrite_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpolar.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cfunctions.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_def.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_ring.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_def.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_cont.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Choice_facts.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/PI.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cseries_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ediff/Evect.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_def.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Canalysis_basic_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nnewton.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_usual.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def_simpl.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_usual.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nfinite_prod.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/MyNeq.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_base_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Cauchy_lipschitz.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpser_def.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Ctacfield.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/MyNat.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_def.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Choice_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Triangular.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Zlittle_fermat.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_def.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_usual.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_remainder_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ediff/realisation_by_stdlib.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_def.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_def.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/InhabitedTactics.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_MVT.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cdefinitions.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rextensionality.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_facts.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cseries.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Ninductions.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_pos_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Npow.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ediff/integrales.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_usual.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Csequence_def.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_ring.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpow.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_bound_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_tactic.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/CFsequence.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Zprime.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/RFsequence.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_tactic.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_examples.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Ctacfield.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Zpow.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Tactics.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Finite_Calculus/Definitions.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Zeqm.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Examples.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Functions.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_def.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cpser_def.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_def.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_usual.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Monad.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_def.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Cseries.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/PI.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Monad/Option.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyR_dist.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nle.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Ntools.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/MyNat.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Complex.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/MyZ.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_def.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbasic_fun.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Ntools.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nminus.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbase.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyReals.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nle.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyNNR.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_stdlib.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ediff/Vectorial_Cauchy.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Choice_facts.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyINR.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/MyNeq.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbasic_fun.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Ninductions.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/InhabitedTactics.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rpser.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/InhabitedTactics.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Complex.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_stdlib.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/MyZ.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyNNR.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyINR.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Rseries.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyReals.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbase.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Csequence.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Arith/Nminus.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/mytheories/MyNeq.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Tactics.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Reals/Tactics.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Coqtail/Complex/Csequence.v
opam remove -y coq-coqtail.8.14