# 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" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-corn.1.0.0 coq.8.4.5
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-corn.1.0.0 coq.8.4.5
opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-corn.1.0.0 coq.8.4.5
Total: 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.vo
opam remove -y coq-corn.1.0.0