# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-ocamlbuild base OCamlbuild binary and libraries distributed with the OCaml compiler
base-threads base
base-unix base
camlp5 7.14 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
conf-perl 2 Virtual package relying on perl
coq 8.7.0 Formal proof management system
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.02.3 The OCaml compiler (virtual package)
ocaml-base-compiler 4.02.3 Official 4.02.3 release
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.6 A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "b.a.w.spitters@gmail.com"
homepage: "https://github.com/coq-community/corn"
dev-repo: "git+https://github.com/coq-community/corn.git"
bug-reports: "https://github.com/coq-community/corn/issues"
license: "GPL-2.0-only"
synopsis: "The Coq Constructive Repository at Nijmegen"
description: """
CoRN includes the following parts:
- Algebraic Hierarchy
An axiomatic formalization of the most common algebraic
structures, including setoids, monoids, groups, rings,
fields, ordered fields, rings of polynomials, real and
complex numbers
- Model of the Real Numbers
Construction of a concrete real number structure
satisfying the previously defined axioms
- Fundamental Theorem of Algebra
A proof that every non-constant polynomial on the complex
plane has at least one root
- Real Calculus
A collection of elementary results on real analysis,
including continuity, differentiability, integration,
Taylor's theorem and the Fundamental Theorem of Calculus
- Exact Real Computation
Fast verified computation inside Coq. This includes: real numbers, functions,
integrals, graphs of functions, differential equations.
"""
build: [
["./configure.sh"]
[make "-j%{jobs}%"]
]
install: [make "install"]
depends: [
"coq" {>= "8.7" & < "8.13~"}
"coq-math-classes" {>= "8.8.1"}
"coq-bignums"
]
tags: [
"category:Mathematics/Algebra"
"category:Mathematics/Real Calculus and Topology"
"category:Mathematics/Exact Real computation"
"keyword:constructive mathematics"
"keyword:algebra"
"keyword:real calculus"
"keyword:real numbers"
"keyword:Fundamental Theorem of Algebra"
"logpath:CoRN"
"date:2020-09-03"
]
authors: [
"Evgeny Makarov"
"Robbert Krebbers"
"Eelis van der Weegen"
"Bas Spitters"
"Jelle Herold"
"Russell O'Connor"
"Cezary Kaliszyk"
"Dan Synek"
"Luís Cruz-Filipe"
"Milad Niqui"
"Iris Loeb"
"Herman Geuvers"
"Randy Pollack"
"Freek Wiedijk"
"Jan Zwanenburg"
"Dimitri Hendriks"
"Henk Barendregt"
"Mariusz Giero"
"Rik van Ginneken"
"Dimitri Hendriks"
"Sébastien Hinderer"
"Bart Kirkels"
"Pierre Letouzey"
"Lionel Mamane"
"Nickolay Shmyrev"
"Vincent Semeria"
]
url {
src: "https://github.com/coq-community/corn/archive/8.12.0.tar.gz"
checksum: "sha512=759ab0e0fc4b4ee8b6029d0090cf8b7ee731def85aacc9d240dfb29d4692e4f41821463f8d8180202587ee9b7c9239be8512c24b0594537e56aa235f31923ec3"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-corn.8.12.0 coq.8.7.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-corn.8.12.0 coq.8.7.0opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-corn.8.12.0 coq.8.7.0Total: 66 M
../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/LinfMetricMonad.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARArith.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRArith.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/Picard.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRFieldOps.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/FieldReflection.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPolynomials.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/csetoid_rewrite.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/iso_CReals.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRArith.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/MultivariatePolynomials.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Compact.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/AbstractIntegration.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/RingReflection.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/NRootCC.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/metric.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/MultivariatePolynomials.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Compact.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPolynomials.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARroot.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/AbstractIntegration.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRFieldOps.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Classified.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefSeparating.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefSeparating.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/SimpleIntegration.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRroot.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARAlternatingSum.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CMonoids.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/Exponential.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/FieldReflection.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ApproximateRationals.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefLemma.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CRings.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Integration.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Series.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRroot.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Complete.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Integral.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Integral.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRexp.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRsin.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/SimpleIntegration.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Integration.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreIntervals.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARsin.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZGcd.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRGeometricSum.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRcorrect.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/InvTrigonom.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Bridges_LUB.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_Newton.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/StepQsec.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefSeparated.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Bridges_iso.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRGeometricSum.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARexp.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Complete.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARArith.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZGcd.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CRings.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARbigD.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_Degree.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdFields.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/CLogic.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Series.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/Exponential.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/ProductMetric.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/FinEnum.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreIntervals.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpi_fast.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/TaylorLemma.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/RingReflection.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/Bernstein.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Interval.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRGroupOps.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Max_AbsIR.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARarctan.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/RasterizeQ.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpi_slow.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/Pi.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/Pi.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreFunctions.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/Cauchy_COF.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Bridges_LUB.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/StepFunction.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefSepRef.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/CPoly_Euclid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdFields.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/coq_reals/Rreals_iso.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRln.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Cauchy_CReals.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdFields2.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/BanachFixpoint.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefLemma.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/L1metric.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/FromMetric2.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/CComplex.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/StepFunctionSetoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRcos.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/AQmetric.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARcos.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/Qmetric.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/COrdLemmas.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/StrongIVT.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Partitions.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefSeparated.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FunctSequence.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRcorrect.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/TrigMon.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Intervals.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRartanh_slow.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/KneserLemma.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRarctan.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Continuity.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/WeakIVT.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARarctan_small.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRexp.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSetoids.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/Picard.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Max_AbsIR.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Composition.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRabs.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Plot.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Composition.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpower.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/Cauchy_COF.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/MainLemma.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRGroupOps.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZDivides.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARpi.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRstreams.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Bridges_iso.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/Expon.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/DerivativeOps.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/RealPowers.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FunctSequence.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Continuity.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Intervals.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/InvTrigonom.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRIR.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRarctan_small.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/CMetricSpaces.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/coq_reals/Rreals_iso.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRsum.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_ApZero.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreFunctions.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Q_dense.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARroot.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/CLogic.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum_alg.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Qdlog.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreFunSeries.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZMod.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/StepFunctionSetoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CFields.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Q_dense.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARabs.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/iso_CReals.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/RasterQ.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/FTAreg.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/CPMSTheory.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdFields2.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/ModulusDerivative.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Graph.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Prelength.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Interval.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FunctSeries.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Rolle.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Limit.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/Trigonometric.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARbigQ.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/RealPowers.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/TaylorSeries.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/TaylorLemma.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/MoreArcTan.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Classified.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSums.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/AlgReflection.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_Newton.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/TrigMon.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSums.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Q_in_CReals.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARSpeedTests.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/Expon.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSetoidFun.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/NRootIR.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/WeakIVTQ.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/reals/CRreal.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreFunSeries.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/NRootIR.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/NRootCC.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZBasics.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpower.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdCauchy.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/CornBasics.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARtrans.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Graph.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/ContinuousCorrect.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CPoly_Rev.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/metric.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/MoreArcTan.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/MetricMorphisms.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/DerivativeOps.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Extract.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/LinfDistMonad.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/DistanceMetricSpace.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreIntegrals.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/NNUpperR.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/Trigonometric.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/TaylorSeries.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/KneserLemma.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/KeyLemma.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/LinfMetric.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/ArTanH.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/Liouville.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Q_in_CReals.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/PowerSeries.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRtrans.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FunctSums.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/NthDerivative.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/SinCos.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/Bernstein.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefSepRef.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/CalculusTheorems.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/coq_reals/Rsign.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/LocatedSubset.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdCauchy.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_ApZero.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpi.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRball.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/totalorder/QposMinMax.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CauchySeq.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRsin.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRArith_alg.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Qsums.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/CalculusTheorems.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/ContFunctions.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/IR_CPMSpace.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/uneven_CRplus.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/MainLemma.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Rolle.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CFields.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/RasterizeQ.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARQ.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Compress.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Cauchy_CReals.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/IVT.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Taylor.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FunctSeries.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/StepFunction.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRsign.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/DiffTactics2.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_Degree.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/ContFunctions.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/AbsCC.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARsign.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/LipExt.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/Q.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/QX_root_loc.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/RealCount.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Qinf.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreIntegrals.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CMonoids.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/LipExt.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/StepFunctionMonad.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CauchySeq.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CGroups.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/Stability.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Qpossec.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSetoids.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FTC.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CAbGroups.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdAbs.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/FTAreg.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/rings/CRring.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/PartFunEquality.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/QX_extract_roots.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/QX_ZX.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/CPMSTheory.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/ordfields/CRordfield.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Derivative.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/CMetricSpaces.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Partitions.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/AbsCC.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZMod.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/CornBasics.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZDivides.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/PowerSeries.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/ArTanH.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/Liouville.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/Equiv.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/fields/CRfield.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/Complex_Exponential.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/CRgroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/CRsemigroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/CRmonoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/lattice/CRlattice.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/IVT.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/CRsetoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/R_morphism.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Prelength.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/CRabgroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FTC.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/NNUpperR.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/RingClass.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/StrongIVT.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CC_Props.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/OddPolyRootIR.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/IntegrableFunction.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/classes/Qposclasses.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/BoundedFunction.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/KeyLemma.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/Q.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Differentiability.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_NthCoeff.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Taylor.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Ranges.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/FinEnum.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CReals1.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/IntegrationRules.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/Equiv.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARAlternatingSum.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/partialorder/CRpartialorder.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/UniformContinuity.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRArith.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/CRmetric.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/RealLists.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/IR_CPMSpace.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/CompleteProduct.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/totalorder/QposMinMax.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/classes/Qclasses.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdAbs.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRconst.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CReals1.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/csetoid_rewrite.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpi_fast.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/Prod_Sub.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CSumsReals.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARbigD.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CPoly_Rev.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/OpenUnit.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/coq_reals/Rreals.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPolynomials.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CMetricFields.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/CPseudoMSpaces.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/WeakIVT.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CRing_Homomorphisms.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CPoly_Shift.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/DiffTactics3.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CAbGroups.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/FTA.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpi_slow.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/IntervalFunct.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/Zm.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/totalorder/ZMinMax.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/RX_deg.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/totalorder/QMinMax.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/COrdLemmas.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRln.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/PartInterval.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/L1metric.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZBasics.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/RealFuncts.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRartanh_slow.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/QX_root_loc.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/NthDerivative.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Limit.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRabs.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Qsec.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/QnonNeg.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Plot.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/Qmetric.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSetoidFun.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/CComplex.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/IrrCrit.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CPoly_Contin1.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Hausdorff.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/MetricMorphisms.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Cesaro.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRFieldOps.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Compact.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/PosSeq.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSemiGroups.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_NthCoeff.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/nat_Q_lists.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/RX_div.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/totalorder/QMinMax.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Metric.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CGroups.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CPoly_Contin.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/AlgReflection.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/R_morphism.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FunctSums.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Qdlog.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/csetoid_rewrite.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/PartialOrder.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/Q_can.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/LinfMetricMonad.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRsum.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/PowerBound.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/AbstractIntegration.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Qgcd.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/QnnInf.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/Zlcm.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/ProductMetric.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Qpossetoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/QposInf.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/RSetoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/StepFunctionMonad.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/SinCos.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/BanachFixpoint.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/TotalOrder.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRstreams.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/decsetoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/rings/Qring.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRarctan.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/iso_CReals.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRIR.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Derivative.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/MultivariatePolynomials.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/Complex_Exponential.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Zsec.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Integral.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARsin.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/raster/Raster.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/CRingClass.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/ordfields/Qordfield.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/TotalOrder.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/QSposmonoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/Qposgroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/QSposgroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRarctan_small.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum_alg.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Zsec.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ApproximateRationals.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/Cmod.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Qposmonoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/FTA.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/Qposabgroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_freem.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Qsetoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/ModulusDerivative.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/QSposabgroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/IrrCrit.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Zfinsetoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/List.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/Qauto.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/reals/Cauchy_IR.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRcos.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/StepQsec.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZGcd.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/NRootCC.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/totalorder/ZMinMax.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/PartFunEquality.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Cesaro.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/LinfDistMonad.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Qpossemigroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CAbMonoids.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Nsetoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/QSpossemigroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CReals.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Nfinsetoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/fields/Qfield.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Qmonoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Nsec.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreIntervals.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CPoly_Shift.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefSeparating.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/Qgroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_cycm.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSetoidInc.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/RealCount.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Zsetoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/Z.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/Qabgroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/Rational.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/OddPolyRootIR.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/reals/CRreal.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/SemiLattice.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Complete.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/freem_to_Nm.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/OperationClasses.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Classification.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Npossetoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Classified.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Zmonoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Qsemigroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARexp.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRGeometricSum.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Series.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/Exponential.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CRing_as_Ring.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/QX_ZX.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/rings/Zring.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/CPoly_Euclid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/RealLists.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nposmonoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/CLogic.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/InvTrigonom.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/Zgroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CornScope.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/Zabgroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/IntegrationRules.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Npossemigroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nmonoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/UCFnMonoid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdFields.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/FromMetric2.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Npossec.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CC_Props.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/metric.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/RasterQ.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Zsemigroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/FieldReflection.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Bridges_iso.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Integration.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Max_AbsIR.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreFunctions.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefLemma.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Nsemigroup.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/QX_extract_roots.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Differentiability.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/Zm.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRroot.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/Lattice.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/Cauchy_COF.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/Picard.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Compress.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CRings.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/Prod_Sub.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Qsums.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FunctSequence.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Continuity.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/RingReflection.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Intervals.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARArith.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreFunSeries.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Bridges_LUB.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/SetoidPermutation.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/SimpleIntegration.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Composition.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/Pi.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Qpossec.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/list_separates.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSetoids.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/OperationClasses.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRcorrect.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/UniformContinuity.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Hausdorff.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARarctan_small.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/Zlcm.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/coq_reals/Rreals.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdFields2.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/StepFunctionSetoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefSeparated.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARarctan.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/DiffTactics2.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CauchySeq.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Cauchy_CReals.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Qsec.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRexp.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CSumsReals.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/PointFree.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/TaylorLemma.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSetoidFun.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/StepFunction.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/AQmetric.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/CalculusTheorems.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/QnonNeg.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FunctSeries.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/TrigMon.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/FinEnum.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Partitions.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CMetricFields.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/coq_reals/Rreals_iso.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CPoly_Contin1.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Q_in_CReals.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZDivides.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/ContinuousCorrect.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/NRootIR.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSums.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CRing_Homomorphisms.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/RX_deg.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdCauchy.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRGroupOps.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/LocatedSubset.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_Newton.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefSepRef.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Rolle.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CFields.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Q_dense.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CMonoids.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/CornBasics.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreIntegrals.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/TaylorSeries.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSemiGroups.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/NthDerivative.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/PosSeq.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/rings/CRring.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpower.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/LazyNat.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/LinfMetric.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/Pair.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/DerivativeOps.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/IntervalFunct.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/CPseudoMSpaces.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Interval.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/Expon.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/Trigonometric.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZBasics.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Prelength.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_Degree.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/CComplex.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FTC.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/nat_Q_lists.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/CMetricSpaces.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Graph.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/RealPowers.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/raster/Raster.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/StrongIVT.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/CPMSTheory.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/Classic.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/PartialOrder.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRball.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/MoreArcTan.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/DistanceMetricSpace.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/WeakIVT.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/RingClass.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/KneserLemma.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARabs.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZMod.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/P.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/WeakIVTQ.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/Bernstein.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/Lattice.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRsin.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_ApZero.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Container.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/COrdLemmas.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARroot.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/OpenUnit.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/ContFunctions.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/PowerSeries.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/Q_can.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/RasterizeQ.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Metric.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/totalorder/QposMinMax.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/AlgReflection.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/SemiLattice.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/PartInterval.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/lattice/CRlattice.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/FTAreg.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/IVT.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdAbs.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/MainLemma.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FunctSums.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/ArTanH.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/L1metric.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Hausdorff.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/NNUpperR.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/AbsCC.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/RSetoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/Liouville.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRstreams.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/Stability.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/Q.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CReals1.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/PartFunEquality.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/Z.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/Qmetric.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CAbGroups.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/ProductMetric.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CGroups.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/LinfMetricMonad.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/Equiv.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Taylor.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/List.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARAlternatingSum.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/uneven_CRplus.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/Zm.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARbigQ.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/R_morphism.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRartanh_slow.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CPoly_Rev.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/IR_CPMSpace.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Limit.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/LipExt.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRln.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Plot.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/KeyLemma.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/CompleteProduct.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/PowerBound.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/SetoidPermutation.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/QX_root_loc.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_NthCoeff.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Derivative.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/RealLists.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/DiffTactics3.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/StepFunctionMonad.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/QnnInf.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/N.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/QX_ZX.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/MetricMorphisms.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/DiffTactics2.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARpi.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Nsetoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/coq_reals/Rreals.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRabs.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRarctan.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Differentiability.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Qgcd.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpi_fast.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/rings/Qring.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/QposInf.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/LinfDistMonad.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/SinCos.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRIR.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Qpossec.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/Classic.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpi_slow.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/totalorder/QMinMax.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/Prod_Sub.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/IntegrationRules.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Nsec.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARcos.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/FromMetric2.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/UniformContinuity.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CPoly_Contin.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARbigD.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/StepQsec.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Qdlog.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/TotalOrder.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/ModulusDerivative.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/RealFuncts.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/ordfields/CRordfield.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/RealCount.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/QX_extract_roots.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRsum.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/CRsemigroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/totalorder/ZMinMax.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum_alg.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Zsec.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRcos.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/fields/CRfield.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/IrrCrit.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/LocatedSubset.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/decsetoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Qsec.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/OddPolyRootIR.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSemiGroups.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/BanachFixpoint.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/RasterQ.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/CPoly_Euclid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/Pair.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CC_Props.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSetoidInc.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/Cmod.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ApproximateRationals.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/FTA.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/CRgroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/Complex_Exponential.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/RealFuncts.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARexp.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARsin.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/CPseudoMSpaces.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/Zlcm.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/reals/CRreal.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Cesaro.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/IntervalFunct.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/lattice/CRlattice.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRarctan_small.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/RX_deg.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Zsetoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Compress.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Qsums.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/PointFree.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_cycm.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/LinfMetric.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/QnonNeg.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Qinf.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/PartInterval.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CPoly_Shift.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/list_separates.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Qsetoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/OperationClasses.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRArith_alg.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/LazyNat.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/OpenUnit.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/nat_Q_lists.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Metric.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/ContinuousCorrect.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/raster/Raster.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CSumsReals.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Npossec.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/CornTac.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/DiffTactics3.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Nsetoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/RingClass.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/RSetoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARQ.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_freem.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/WeakIVTQ.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CRing_Homomorphisms.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Qpossetoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/PartialOrder.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/Q_can.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/AQmetric.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/QposInf.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/DistanceMetricSpace.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CPoly_Contin1.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/Lattice.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/PosSeq.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/rings/CRring.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARarctan.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/CRmonoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Zfinsetoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CMetricFields.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/SemiLattice.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/CompleteProduct.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Nsec.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CAbMonoids.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Nfinsetoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/PowerBound.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/RX_div.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Zsetoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CPoly_Contin.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/CRingClass.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/Classic.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/P.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Qpossetoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Classification.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARarctan_small.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Ranges.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Npossetoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/Stability.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/List.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Extract.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARabs.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/ordfields/CRordfield.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Qsetoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/SetoidPermutation.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRball.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/CRsetoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/rings/Qring.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/Z.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSetoidInc.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_freem.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/LazyNat.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARbigQ.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRsign.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/Cmod.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/fields/CRfield.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/ordfields/Qordfield.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_cycm.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRArith_alg.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/QnnInf.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/CRsemigroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/uneven_CRplus.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Zmonoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/PointFree.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Npossetoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Zfinsetoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/CRabgroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/decsetoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/CRgroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CAbMonoids.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Zmonoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Nfinsetoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Qgcd.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Classification.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/classes/Qclasses.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/CRingClass.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Qmonoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/Step.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Qmonoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Npossec.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Qinf.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/CRmetric.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/CRsetoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nmonoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/CRmonoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARcos.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/Rational.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/liouville/RX_div.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nmonoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Npossemigroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/ordfields/Qordfield.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/PropDecid.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRconst.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CReals.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/freem_to_Nm.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CReals.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nposmonoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Zsemigroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/QSposmonoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/Qauto.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/CornTac.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARpi.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/classes/Qposclasses.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/IntegrableFunction.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/CRabgroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Qposmonoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/rings/Zring.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Nsemigroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARQ.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/CRmetric.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/Rational.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/DiffTactics1.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/QSposgroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRsign.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/QSposabgroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/Zgroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/BoundedFunction.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Qsemigroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/partialorder/CRpartialorder.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/fields/Qfield.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/Zabgroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/Qgroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/PropDecid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/Qposgroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/list_separates.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/freem_to_Nm.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/Qabgroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRtrans.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/reals/Cauchy_IR.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/Qposabgroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/IntegrableFunction.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/QSpossemigroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Zsemigroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/DiffTactics1.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Qpossemigroup.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/UCFnMonoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nposmonoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/Step.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARsign.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CornScope.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/partialorder/CRpartialorder.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/P.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Npossemigroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/QSposmonoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Qposmonoid.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/Pair.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Nsemigroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/rings/Zring.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CornScope.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/Qgroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/PropDecid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARsign.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/BoundedFunction.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRconst.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CRing_as_Ring.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARSpeedTests.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Ranges.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/coq_reals/Rsign.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/Zgroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/coq_reals/Rsign.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/Qposgroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/Qauto.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/fields/Qfield.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/QSposgroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Container.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/Qabgroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/Zabgroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Qsemigroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/UCFnMonoid.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Extract.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpi.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/classes/Qclasses.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/QSposabgroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/Qposabgroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRtrans.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/classes/Qposclasses.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/N.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Qpossemigroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpi.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARSpeedTests.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/QSpossemigroup.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARtrans.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/reals/Cauchy_IR.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARtrans.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/CornTac.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Container.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CRing_as_Ring.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/N.v../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/DiffTactics1.glob../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/Step.globopam remove -y coq-corn.8.12.0