« Up

corn 1.0.0 2 h 3 m 🏆

Context

# 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
camlp4              4.02+7       Camlp4 is a system for writing extensible parsers for programming languages
conf-findutils      1            Virtual package relying on findutils
conf-which          1            Virtual package relying on which
coq                 8.4.6~camlp4 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"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-corn.1.0.0 coq.8.4.6~camlp4
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-corn.1.0.0 coq.8.4.6~camlp4
Return code
0
Duration
17 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-corn.1.0.0 coq.8.4.6~camlp4
Return code
0
Duration
2 h 3 m

Installation size

Total: 41 M

  • 5 M ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefLemma.vo
  • 3 M ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/LinfMetricMonad.vo
  • 1 M ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARArith.vo
  • 961 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/TaylorLemma.vo
  • 626 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefSeparated.vo
  • 469 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPolynomials.vo
  • 444 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/FieldReflection.vo
  • 428 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/Picard.vo
  • 425 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefSeparating.vo
  • 382 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/AbstractIntegration.vo
  • 353 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/MultivariatePolynomials.vo
  • 349 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CMonoids.vo
  • 342 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/metric.vo
  • 341 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/RingReflection.vo
  • 339 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/NRootCC.vo
  • 329 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Compact.vo
  • 325 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARroot.vo
  • 315 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/csetoid_rewrite.vo
  • 305 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Bridges_LUB.vo
  • 298 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/COrdLemmas.vo
  • 269 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARsin.vo
  • 267 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CRings.vo
  • 264 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Integral.vo
  • 261 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdFields.vo
  • 253 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/StrongIVT.vo
  • 248 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/Bernstein.vo
  • 244 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/SimpleIntegration.vo
  • 242 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ApproximateRationals.vo
  • 241 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZGcd.vo
  • 233 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_Degree.vo
  • 221 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreIntervals.vo
  • 221 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARAlternatingSum.vo
  • 221 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/Exponential.vo
  • 220 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Bridges_iso.vo
  • 216 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/WeakIVT.vo
  • 211 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/Cauchy_COF.vo
  • 209 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRroot.vo
  • 206 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/KneserLemma.vo
  • 205 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Max_AbsIR.vo
  • 202 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZMod.vo
  • 198 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/FTAreg.vo
  • 197 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Series.vo
  • 194 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/CLogic.vo
  • 193 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CFields.vo
  • 191 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/Pi.vo
  • 191 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARbigD.vo
  • 189 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreIntegrals.vo
  • 186 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/MainLemma.vo
  • 186 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRArith.vo
  • 186 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/RefSepRef.vo
  • 185 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/StepQsec.vo
  • 184 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRsin.vo
  • 183 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/IVT.vo
  • 183 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRcorrect.vo
  • 182 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/coq_reals/Rreals_iso.vo
  • 182 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/Trigonometric.vo
  • 179 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARexp.vo
  • 178 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Continuity.vo
  • 177 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARcos.vo
  • 176 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRexp.vo
  • 176 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/WeakIVTQ.vo
  • 176 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreFunctions.vo
  • 173 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/FromMetric2.vo
  • 173 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_ApZero.vo
  • 171 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSetoids.vo
  • 171 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Complete.vo
  • 169 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/FinEnum.vo
  • 168 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/StepFunctionSetoid.vo
  • 168 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Composition.vo
  • 167 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FunctSequence.vo
  • 167 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Partitions.vo
  • 167 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/CComplex.vo
  • 165 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Integration.vo
  • 165 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZDivides.vo
  • 164 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/MoreFunSeries.vo
  • 164 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/NRootIR.vo
  • 160 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdFields2.vo
  • 160 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/StepFunction.vo
  • 159 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Q_dense.vo
  • 158 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ode/BanachFixpoint.vo
  • 157 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRGeometricSum.vo
  • 157 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARarctan_small.vo
  • 156 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRFieldOps.vo
  • 156 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/MoreArcTan.vo
  • 153 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Intervals.vo
  • 153 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/InvTrigonom.vo
  • 148 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/RealPowers.vo
  • 146 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/KeyLemma.vo
  • 145 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/MetricMorphisms.vo
  • 145 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/AQmetric.vo
  • 142 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/CalculusTheorems.vo
  • 142 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FunctSeries.vo
  • 141 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpi_fast.vo
  • 141 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARarctan.vo
  • 140 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/TaylorSeries.vo
  • 136 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FunctSums.vo
  • 135 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/TrigMon.vo
  • 133 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Interval.vo
  • 131 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/RasterizeQ.vo
  • 130 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/NthDerivative.vo
  • 128 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpi_slow.vo
  • 128 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdCauchy.vo
  • 127 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/R_morphism.vo
  • 125 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/CornBasics.vo
  • 124 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Prelength.vo
  • 123 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/DerivativeOps.vo
  • 123 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/Expon.vo
  • 123 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/NNUpperR.vo
  • 123 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/iso_CReals.vo
  • 120 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSums.vo
  • 118 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/CPMSTheory.vo
  • 117 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum.vo
  • 115 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Taylor.vo
  • 114 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSetoidFun.vo
  • 113 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Rolle.vo
  • 112 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/LipExt.vo
  • 112 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CauchySeq.vo
  • 112 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Cauchy_CReals.vo
  • 111 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/L1metric.vo
  • 110 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/Complex_Exponential.vo
  • 110 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/PowerSeries.vo
  • 110 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Graph.vo
  • 109 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/ZBasics.vo
  • 109 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CPoly_Rev.vo
  • 109 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/OddPolyRootIR.vo
  • 109 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/RealCount.vo
  • 108 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRseries.vo
  • 108 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/AlgReflection.vo
  • 106 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/SinCos.vo
  • 105 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/COrdAbs.vo
  • 101 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRGroupOps.vo
  • 100 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Q_in_CReals.vo
  • 99 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Limit.vo
  • 98 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/transc/ArTanH.vo
  • 97 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRcos.vo
  • 97 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/DiffTactics2.vo
  • 97 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/FTC.vo
  • 96 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRln.vo
  • 95 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CGroups.vo
  • 93 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/PartFunEquality.vo
  • 93 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/complex/AbsCC.vo
  • 93 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CMetricFields.vo
  • 93 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Qdlog.vo
  • 91 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Derivative.vo
  • 90 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CAbGroups.vo
  • 88 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Metric.vo
  • 88 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/Qmetric.vo
  • 87 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/IntegrationRules.vo
  • 84 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARpi.vo
  • 84 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRIR.vo
  • 83 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CReals1.vo
  • 83 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/StepFunctionMonad.vo
  • 83 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/Q.vo
  • 80 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRarctan.vo
  • 80 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRsum.vo
  • 79 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/ContFunctions.vo
  • 79 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/ModulusDerivative.vo
  • 78 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/ProductMetric.vo
  • 77 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Qpossec.vo
  • 77 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/RasterQ.vo
  • 76 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CPoly_NthCoeff.vo
  • 75 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/IntervalFunct.vo
  • 74 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpower.vo
  • 72 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/TotalOrder.vo
  • 71 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CC_Props.vo
  • 70 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/PartialOrder.vo
  • 69 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CSumsReals.vo
  • 69 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/UniformContinuity.vo
  • 68 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/coq_reals/Rreals.vo
  • 68 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRarctan_small.vo
  • 68 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/Differentiability.vo
  • 68 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/CMetricSpaces.vo
  • 68 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRabs.vo
  • 67 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/RealLists.vo
  • 64 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CRing_Homomorphisms.vo
  • 63 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/reals/CRreal.vo
  • 63 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/FTA.vo
  • 61 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/ftc/PartInterval.vo
  • 60 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/RSetoid.vo
  • 60 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRartanh_slow.vo
  • 60 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/totalorder/QposMinMax.vo
  • 59 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/IR_CPMSpace.vo
  • 58 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/Equiv.vo
  • 58 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARbigQ.vo
  • 57 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Plot.vo
  • 57 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/totalorder/ZMinMax.vo
  • 57 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/totalorder/QMinMax.vo
  • 57 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/Cesaro.vo
  • 56 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/QnonNeg.vo
  • 56 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/LinfDistMonad.vo
  • 55 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/Zm.vo
  • 55 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/CPseudoMSpaces.vo
  • 55 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Qsums.vo
  • 55 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/Compress.vo
  • 54 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/OpenUnit.vo
  • 53 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/ContinuousCorrect.vo
  • 52 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/SemiLattice.vo
  • 52 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRball.vo
  • 51 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/LinfMetric.vo
  • 51 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/DiffTactics3.vo
  • 50 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CPoly_Shift.vo
  • 50 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/fta/CPoly_Contin1.vo
  • 50 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/Cmod.vo
  • 50 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/PowerBound.vo
  • 50 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metrics/Prod_Sub.vo
  • 49 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/DistanceMetricSpace.vo
  • 49 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/OperationClasses.vo
  • 48 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Qsec.vo
  • 48 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Hausdorff.vo
  • 48 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/Stability.vo
  • 47 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSemiGroups.vo
  • 45 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/order/Lattice.vo
  • 44 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/RealFuncts.vo
  • 44 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/uneven_CRplus.vo
  • 43 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/lattice/CRlattice.vo
  • 42 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/Zmod/IrrCrit.vo
  • 42 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARQ.vo
  • 42 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Qinf.vo
  • 41 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/QnnInf.vo
  • 41 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/decsetoid.vo
  • 41 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/CompleteProduct.vo
  • 41 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CPoly_Contin.vo
  • 39 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Extract.vo
  • 38 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/List.vo
  • 38 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/PosSeq.vo
  • 38 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Qgcd.vo
  • 37 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Zsec.vo
  • 37 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/coq_reals/Rsign.vo
  • 37 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/QposInf.vo
  • 37 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/raster/Raster.vo
  • 35 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/rings/CRring.vo
  • 35 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARtrans.vo
  • 34 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRtrans.vo
  • 34 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/faster/ARsign.vo
  • 34 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/ordfields/CRordfield.vo
  • 34 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRpi.vo
  • 33 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Nsec.vo
  • 32 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/fields/CRfield.vo
  • 31 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/CReals.vo
  • 31 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/CRgroup.vo
  • 31 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/Classification.vo
  • 31 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRsign.vo
  • 31 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/CRsemigroup.vo
  • 30 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/CRmonoid.vo
  • 30 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/CRsetoid.vo
  • 30 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Zfinsetoid.vo
  • 29 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Qpossetoid.vo
  • 29 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/CRabgroup.vo
  • 29 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/CRmetric.vo
  • 29 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CAbMonoids.vo
  • 28 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/CRconst.vo
  • 28 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/partialorder/CRpartialorder.vo
  • 28 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/IntegrableFunction.vo
  • 28 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_freem.vo
  • 28 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/Z.vo
  • 27 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Nfinsetoid.vo
  • 27 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/metric2/BoundedFunction.vo
  • 27 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/SetoidPermutation.vo
  • 27 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Nsetoid.vo
  • 27 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/classes/Qposclasses.vo
  • 27 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/rings/Qring.vo
  • 25 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/classes/Qclasses.vo
  • 25 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/ordfields/Qordfield.vo
  • 24 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CSetoidInc.vo
  • 24 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/Qauto.vo
  • 23 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/UCFnMonoid.vo
  • 23 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_cycm.vo
  • 23 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/structures/Npossec.vo
  • 23 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Qsetoid.vo
  • 23 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/QSposmonoid.vo
  • 23 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/QSposgroup.vo
  • 22 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/Qposgroup.vo
  • 22 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Npossetoid.vo
  • 22 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CRing_as_Ring.vo
  • 21 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Qposmonoid.vo
  • 21 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/setoids/Zsetoid.vo
  • 21 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/Rational.vo
  • 21 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/QSposabgroup.vo
  • 21 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/Qposabgroup.vo
  • 20 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Qmonoid.vo
  • 20 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/freem_to_Nm.vo
  • 20 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/reals/Cauchy_IR.vo
  • 19 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Qpossemigroup.vo
  • 19 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/QSpossemigroup.vo
  • 19 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/fields/Qfield.vo
  • 19 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Zmonoid.vo
  • 19 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/Qgroup.vo
  • 18 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nposmonoid.vo
  • 18 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/Qabgroup.vo
  • 18 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/monoids/Nmonoid.vo
  • 18 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/rings/Zring.vo
  • 18 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/algebra/CornScope.vo
  • 18 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/PointFree.vo
  • 18 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Npossemigroup.vo
  • 18 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Qsemigroup.vo
  • 17 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/groups/Zgroup.vo
  • 17 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/abgroups/Zabgroup.vo
  • 17 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Zsemigroup.vo
  • 17 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/model/semigroups/Nsemigroup.vo
  • 14 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/Pair.vo
  • 12 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/reals/fast/LazyNat.vo
  • 12 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/Classic.vo
  • 10 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/P.vo
  • 6 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/util/Container.vo
  • 4 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/CornTac.vo
  • 2 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/stdlib_omissions/N.vo
  • 2 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/logic/PropDecid.vo
  • 1 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/Step.vo
  • 1 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/tactics/DiffTactics1.vo
  • 1 K ../ocaml-base-compiler.4.02.3/lib/coq/user-contrib/CoRN/metric2/CompletePointFree.vo

Uninstall 🧹

Command
opam remove -y coq-corn.1.0.0
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣