# 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.4.5 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
ocamlbuild 0 Build system distributed with the OCaml compiler since OCaml 3.10.0
# opam file:
opam-version: "2.0"
maintainer: "b.a.w.spitters@gmail.com"
homepage: "http://corn.cs.ru.nl/"
doc: "http://corn.cs.ru.nl/"
authors: "Corn development team"
license: "GPL 2"
build: [
["./configure.sh"]
[make "-j%{jobs}%"]
]
install: [make "install"]
depends: [
"ocaml"
"coq" {>= "8.4pl4" & < "8.5~"}
"coq-math-classes"
]
tags: [
"logpath:CoRN"
]
synopsis: "The CoRN library"
url {
src:
"https://github.com/c-corn/corn/archive/e9162eaba7e705e793aad4dbbffdb606aba9b3bb.tar.gz"
checksum: "md5=868d1b9114497c6d92d7f75a9470b64d"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-corn.1.0.0 coq.8.4.5Dry 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.1.0.0 coq.8.4.5opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-corn.1.0.0 coq.8.4.5Total: 41 M
../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/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/ftc/TaylorLemma.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/algebra/CPolynomials.vo../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/ode/Picard.vo../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/AbstractIntegration.vo../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/fast/MultivariatePolynomials.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/tactics/RingReflection.vo../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/complex/NRootCC.vo../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/reals/faster/ARroot.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/ftc/COrdLemmas.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/algebra/CRings.vo../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/algebra/COrdFields.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/algebra/Bernstein.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/faster/ApproximateRationals.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/algebra/CPoly_Degree.vo../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/ARAlternatingSum.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/reals/Bridges_iso.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/algebra/Cauchy_COF.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/fta/KneserLemma.vo../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/model/Zmod/ZMod.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/reals/Series.vo../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/logic/CLogic.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/reals/faster/ARbigD.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/fta/MainLemma.vo../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/ftc/RefSepRef.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/reals/fast/CRsin.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/reals/fast/CRcorrect.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/transc/Trigonometric.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/ftc/Continuity.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/reals/fast/CRexp.vo../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/ftc/MoreFunctions.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/algebra/CPoly_ApZero.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/algebra/CSetoids.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/metric2/StepFunctionSetoid.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/ftc/FunctSequence.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/complex/CComplex.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/model/Zmod/ZDivides.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/reals/NRootIR.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/metric2/StepFunction.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/ode/BanachFixpoint.vo../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/ARarctan_small.vo../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/transc/MoreArcTan.vo../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/transc/RealPowers.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/metric2/MetricMorphisms.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/ftc/CalculusTheorems.vo../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/reals/fast/CRpi_fast.vo../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/transc/TaylorSeries.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/transc/TrigMon.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/RasterizeQ.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/reals/fast/CRpi_slow.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/reals/R_morphism.vo../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/metric2/Prelength.vo../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/algebra/Expon.vo../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/reals/iso_CReals.vo../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/metrics/CPMSTheory.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/ftc/Taylor.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/ftc/Rolle.vo../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/reals/CauchySeq.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/model/metric2/L1metric.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/transc/PowerSeries.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/model/Zmod/ZBasics.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/reals/OddPolyRootIR.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/tactics/AlgReflection.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRseries.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/COrdAbs.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/reals/fast/CRGroupOps.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/metric2/Limit.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/reals/fast/CRcos.vo../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/reals/fast/CRln.vo../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/ftc/PartFunEquality.vo../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/CMetricFields.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/Derivative.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/metric2/Metric.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/IntegrationRules.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/CRIR.vo../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/metric2/StepFunctionMonad.vo../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/reals/fast/CRarctan.vo../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/metrics/ContFunctions.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/ProductMetric.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/reals/fast/RasterQ.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/IntervalFunct.vo../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/order/TotalOrder.vo../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/order/PartialOrder.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/metric2/UniformContinuity.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/reals/fast/CRarctan_small.vo../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/metrics/CMetricSpaces.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/RealLists.vo../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/model/reals/CRreal.vo../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/ftc/PartInterval.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/reals/fast/CRartanh_slow.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/metrics/IR_CPMSpace.vo../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/reals/faster/ARbigQ.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/model/totalorder/ZMinMax.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/reals/Cesaro.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/model/metric2/LinfDistMonad.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/metrics/CPseudoMSpaces.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/reals/fast/Compress.vo../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/reals/fast/ContinuousCorrect.vo../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/tactics/DiffTactics3.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/metric2/LinfMetric.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/fta/CPoly_Contin1.vo../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/reals/fast/PowerBound.vo../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/metric2/DistanceMetricSpace.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/model/structures/Qsec.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/logic/Stability.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/order/Lattice.vo../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/uneven_CRplus.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/model/Zmod/IrrCrit.vo../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/model/structures/Qinf.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/model/setoids/decsetoid.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/reals/CPoly_Contin.vo../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/stdlib_omissions/List.vo../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/util/Qgcd.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/model/structures/Zsec.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/raster/Raster.vo../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/reals/faster/ARtrans.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/reals/fast/CRtrans.vo../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/reals/fast/CRpi.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/model/fields/CRfield.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/groups/CRgroup.vo../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/metric2/Classification.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/setoids/CRsetoid.vo../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/model/setoids/Qpossetoid.vo../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/model/metric2/CRmetric.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/reals/fast/CRconst.vo../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/model/metric2/IntegrableFunction.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/stdlib_omissions/Z.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/metric2/BoundedFunction.vo../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/model/setoids/Nsetoid.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/rings/Qring.vo../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/tactics/Qauto.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/algebra/CSetoidInc.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/model/monoids/Nm_to_cycm.vo../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/model/setoids/Qsetoid.vo../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/QSposgroup.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/setoids/Npossetoid.vo../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/tactics/Rational.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/model/setoids/Zsetoid.vo../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/abgroups/Qposabgroup.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/monoids/freem_to_Nm.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/model/semigroups/Qpossemigroup.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/model/fields/Qfield.vo../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/groups/Qgroup.vo../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/model/abgroups/Qabgroup.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/model/rings/Zring.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/util/PointFree.vo../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/semigroups/Qsemigroup.vo../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/model/abgroups/Zabgroup.vo../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/model/semigroups/Nsemigroup.vo../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/reals/fast/LazyNat.vo../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/stdlib_omissions/P.vo../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/tactics/CornTac.vo../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/logic/PropDecid.vo../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/tactics/DiffTactics1.vo../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/CompletePointFree.voopam remove -y coq-corn.1.0.0