« Up

corn 8.16.0 51 m 0 s 🏆

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-findutils        1           Virtual package relying on findutils
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   8.15.1      Formal proof management system
dune                  3.6.2       Fast, portable, and opinionated build system
ocaml                 4.14.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.14.0      Official release 4.14.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.5       A library manager for OCaml
zarith                1.12        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "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.11" & < "8.17~"}
  "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:2022-08-20"
]
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.16.0.tar.gz"
  checksum: "sha512=2c2d6f013650e36c2766b7d89a4c40e8f144dd7cc159fea1f130bda84cdec04b30efa29c5144a16be85a4ebc2768a2035fbef5456978245327cf5a5210979bb8"
}

Lint

Command

true

Return code

0

Dry install 🏜️

Dry install with the current Coq version:

Command

opam install -y --show-action coq-corn.8.16.0 coq.8.15.1

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.8.16.0 coq.8.15.1

Return code

0

Duration

10 m 0 s

Install 🚀

Command

opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-corn.8.16.0 coq.8.15.1

Return code

0

Duration

51 m 0 s

Installation size

Total: 58 M

• 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/LinfMetricMonad.vo
• 1013 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Series.vo
• 625 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRArith.glob
• 612 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Rolle.vo
• 551 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARArith.vo
• 436 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRFieldOps.glob
• 404 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/MoreIntervals.vo
• 402 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPolynomials.glob
• 376 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/iso_CReals.glob
• 373 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Compact.glob
• 362 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/FieldReflection.vo
• 358 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/Picard.vo
• 357 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/csetoid_rewrite.vo
• 348 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum.glob
• 318 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/MultivariatePolynomials.glob
• 313 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/InvTrigonom.vo
• 307 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/complex/NRootCC.glob
• 290 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/AbstractIntegration.glob
• 288 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRArith.vo
• 279 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/RingReflection.vo
• 270 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/RefSeparating.glob
• 266 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/MultivariatePolynomials.vo
• 265 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRroot.glob
• 258 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/FieldReflection.glob
• 251 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/Exponential.glob
• 248 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Intervals.vo
• 244 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPolynomials.vo
• 242 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/RefLemma.glob
• 238 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/AbstractIntegration.vo
• 237 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Series.glob
• 236 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARArith.glob
• 235 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/SimpleIntegration.vo
• 233 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Integral.glob
• 228 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/Integration.glob
• 224 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/SimpleIntegration.glob
• 224 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Complete.glob
• 220 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRFieldOps.vo
• 220 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRGeometricSum.glob
• 219 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Compact.vo
• 219 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/metric.vo
• 217 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Bridges_LUB.glob
• 215 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Bridges_iso.glob
• 214 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/InvTrigonom.glob
• 211 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRroot.vo
• 211 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/ZGcd.vo
• 210 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARroot.vo
• 205 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/ZGcd.glob
• 202 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/COrdFields.glob
• 201 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CRings.glob
• 196 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/MoreIntervals.glob
• 195 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/RingReflection.glob
• 190 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Classified.vo
• 190 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRsin.glob
• 185 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Max_AbsIR.glob
• 184 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum.vo
• 184 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CRings.vo
• 181 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRexp.glob
• 176 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/FinEnum.vo
• 175 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/Pi.glob
• 174 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/COrdFields2.glob
• 172 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/Integration.vo
• 170 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Cauchy_CReals.glob
• 167 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Complete.vo
• 165 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Intervals.glob
• 164 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/RefSeparating.vo
• 162 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRcorrect.glob
• 162 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/RefSeparated.glob
• 161 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Integral.vo
• 160 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARroot.glob
• 159 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/KneserLemma.glob
• 159 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ApproximateRationals.vo
• 159 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/TrigMon.glob
• 156 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/StepQsec.vo
• 156 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/Exponential.vo
• 156 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRsin.vo
• 155 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/Picard.glob
• 153 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Composition.glob
• 153 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRcorrect.vo
• 152 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARsin.vo
• 152 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/CLogic.glob
• 151 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/Cauchy_COF.glob
• 150 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/MainLemma.glob
• 150 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRexp.vo
• 149 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/Expon.glob
• 149 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRGroupOps.glob
• 148 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/Pi.vo
• 148 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Continuity.glob
• 148 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/StepFunction.vo
• 146 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/FunctSequence.glob
• 146 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/Bernstein.vo
• 144 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/coq_reals/Rreals_iso.glob
• 144 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/RefSeparated.vo
• 143 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/CLogic.vo
• 143 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/MoreFunctions.glob
• 143 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRGeometricSum.vo
• 143 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/Cauchy_COF.vo
• 142 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Classified.glob
• 142 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARexp.vo
• 141 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPoly_ApZero.glob
• 141 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/CMetricSpaces.glob
• 141 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/COrdFields.vo
• 140 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Q_dense.glob
• 139 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPoly_Newton.vo
• 139 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/MoreFunctions.vo
• 139 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/TaylorLemma.vo
• 137 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/StepFunctionSetoid.vo
• 136 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/complex/CComplex.vo
• 135 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Graph.glob
• 134 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Rolle.glob
• 134 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSums.glob
• 133 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/coq_reals/Rreals_iso.vo
• 132 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/metric.glob
• 132 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Bridges_LUB.vo
• 131 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ACarith.vo
• 130 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/Interval.glob
• 130 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/RealPowers.glob
• 129 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/COrdCauchy.glob
• 129 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/TaylorSeries.glob
• 129 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/TaylorLemma.glob
• 128 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRGroupOps.vo
• 128 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/NRootIR.glob
• 128 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARAlternatingSum.glob
• 128 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Partitions.vo
• 127 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/MoreFunSeries.glob
• 127 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Q_in_CReals.glob
• 126 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/MoreArcTan.glob
• 125 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/FunctSequence.vo
• 125 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRpower.glob
• 123 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSetoids.vo
• 123 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/RefLemma.vo
• 123 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/RasterizeQ.glob
• 123 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Max_AbsIR.vo
• 122 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRpi_fast.vo
• 122 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CMonoids.vo
• 122 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRstreams.vo
• 120 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Bridges_iso.vo
• 120 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARbigD.vo
• 120 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Continuity.vo
• 119 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPoly_Newton.glob
• 119 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/StepFunctionSetoid.glob
• 119 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Composition.vo
• 119 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/DerivativeOps.glob
• 118 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/StrongIVT.vo
• 118 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/Interval.vo
• 117 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/ProductMetric.vo
• 117 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/MoreIntegrals.glob
• 117 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/Trigonometric.glob
• 117 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/AlgReflection.vo
• 116 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/WeakIVT.vo
• 116 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/RealPowers.vo
• 115 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARAlternatingSum.vo
• 114 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Derivative.vo
• 113 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/Bernstein.glob
• 113 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRarctan_small.glob
• 113 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/CalculusTheorems.glob
• 112 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/DerivativeOps.vo
• 112 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/RefSepRef.glob
• 112 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARarctan.vo
• 111 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/L1metric.vo
• 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CFields.glob
• 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/ZDivides.vo
• 109 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/Qmetric.vo
• 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/COrdLemmas.vo
• 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/StepFunction.glob
• 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CFields.vo
• 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRpi_slow.vo
• 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/iso_CReals.vo
• 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/FunctSeries.glob
• 107 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/IR_CPMSpace.glob
• 107 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPoly_Degree.glob
• 107 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Prelength.vo
• 106 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/COrdFields2.vo
• 106 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/MoreFunSeries.vo
• 105 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSetoids.glob
• 105 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CauchySeq.glob
• 105 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Q_dense.vo
• 104 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/ContFunctions.glob
• 104 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPoly_Degree.vo
• 104 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/CPMSTheory.vo
• 103 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/RefSepRef.vo
• 103 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/FinEnum.glob
• 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRln.vo
• 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/RasterizeQ.vo
• 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/LipExt.glob
• 101 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CMonoids.glob
• 100 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Partitions.glob
• 100 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSetoidFun.vo
• 99 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/MoreIntegrals.vo
• 99 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/CPMSTheory.glob
• 99 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/ZBasics.vo
• 98 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/Expon.vo
• 98 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/CornBasics.glob
• 98 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/FunctSeries.vo
• 98 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum_alg.vo
• 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/FTAreg.vo
• 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/FTAreg.glob
• 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRstreams.glob
• 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/AQmetric.vo
• 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/TrigMon.vo
• 96 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/NRootIR.vo
• 96 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRartanh_slow.vo
• 96 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/ZDivides.glob
• 95 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/ZMod.glob
• 95 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSums.vo
• 95 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/MetricMorphisms.vo
• 94 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/MoreArcTan.vo
• 94 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/Trigonometric.vo
• 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/CPoly_Euclid.vo
• 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/BanachFixpoint.vo
• 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/complex/NRootCC.vo
• 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/complex/AbsCC.glob
• 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/FromMetric2.vo
• 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Limit.vo
• 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Prelength.glob
• 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARcos.vo
• 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/IVT.glob
• 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/PowerSeries.glob
• 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/ArTanH.glob
• 91 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/Liouville.glob
• 91 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/Liouville.vo
• 91 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARarctan_small.vo
• 91 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/TaylorSeries.vo
• 91 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/FTC.glob
• 91 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRabs.vo
• 90 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/NNUpperR.vo
• 90 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/NNUpperR.glob
• 89 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/SinCos.vo
• 89 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/StrongIVT.glob
• 88 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRarctan.vo
• 88 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/CalculusTheorems.vo
• 88 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/CornBasics.vo
• 88 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRpower.vo
• 88 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/ArTanH.vo
• 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/COrdCauchy.vo
• 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/Plot.vo
• 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRarctan_small.vo
• 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/KeyLemma.glob
• 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/KneserLemma.vo
• 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Q_in_CReals.vo
• 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CauchySeq.vo
• 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARsin.glob
• 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/Q.glob
• 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/RasterQ.vo
• 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/WeakIVTQ.vo
• 86 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/csetoid_rewrite.glob
• 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPoly_ApZero.vo
• 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/Equiv.glob
• 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Taylor.glob
• 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/PowerSeries.vo
• 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/totalorder/QposMinMax.glob
• 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARpi.vo
• 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRcos.vo
• 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/totalorder/QposMinMax.vo
• 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/FunctSums.vo
• 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/NthDerivative.vo
• 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRArith.v
• 82 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/DiffTactics2.vo
• 82 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/COrdAbs.glob
• 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/RealLists.vo
• 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/CPoly_Rev.glob
• 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/ZMod.vo
• 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/ContFunctions.vo
• 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Cauchy_CReals.vo
• 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/QX_root_loc.vo
• 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CReals1.glob
• 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/COrdLemmas.glob
• 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/Q.vo
• 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARexp.glob
• 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Graph.vo
• 79 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRpi_fast.glob
• 79 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRsum.vo
• 79 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/complex/AbsCC.vo
• 79 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARbigD.glob
• 78 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/IVT.vo
• 77 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/KeyLemma.vo
• 77 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum_alg.glob
• 77 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CGroups.vo
• 76 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/StepFunctionMonad.vo
• 76 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/MainLemma.vo
• 76 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/WeakIVT.glob
• 76 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Qdlog.vo
• 76 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Taylor.vo
• 75 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CAbGroups.glob
• 75 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRIR.vo
• 74 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/COrdAbs.vo
• 74 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRpi_slow.glob
• 74 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CAbGroups.vo
• 74 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Qpossec.vo
• 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPolynomials.v
• 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/ZBasics.glob
• 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/QX_extract_roots.vo
• 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARabs.vo
• 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/QX_ZX.vo
• 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/LipExt.vo
• 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/FTC.vo
• 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Limit.glob
• 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/reals/CRreal.vo
• 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/CPoly_Rev.vo
• 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRartanh_slow.glob
• 71 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRln.glob
• 70 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSetoidFun.glob
• 70 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/ModulusDerivative.vo
• 70 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/CMetricSpaces.vo
• 70 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/NthDerivative.glob
• 70 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/RingClass.vo
• 70 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/L1metric.glob
• 70 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/Equiv.vo
• 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/LocatedSubset.vo
• 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/R_morphism.vo
• 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRabs.glob
• 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/PartFunEquality.vo
• 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/QX_root_loc.glob
• 68 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/LinfMetric.vo
• 68 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/FunctSums.glob
• 67 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/Qmetric.glob
• 67 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/Plot.glob
• 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/LinfDistMonad.vo
• 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/LinfMetricMonad.glob
• 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/complex/CComplex.glob
• 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/totalorder/QMinMax.glob
• 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/MetricMorphisms.glob
• 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPoly_NthCoeff.vo
• 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRsum.glob
• 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Compact.v
• 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/coq_reals/Rreals.vo
• 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPoly_NthCoeff.glob
• 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/complex/Complex_Exponential.vo
• 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRFieldOps.v
• 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CGroups.glob
• 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/AlgReflection.glob
• 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/R_morphism.glob
• 60 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARbigQ.vo
• 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/DistanceMetricSpace.vo
• 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CReals1.vo
• 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/OddPolyRootIR.vo
• 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Qsums.vo
• 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Differentiability.vo
• 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/IntegrationRules.vo
• 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/UniformContinuity.vo
• 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Qdlog.glob
• 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARplot.vo
• 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/CC_Props.vo
• 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/IR_CPMSpace.vo
• 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/ContinuousCorrect.vo
• 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/csetoid_rewrite.v
• 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRarctan.glob
• 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Extract.vo
• 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/RealCount.vo
• 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/LinfDistMonad.glob
• 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/SinCos.glob
• 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/Prod_Sub.vo
• 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/AbstractIntegration.v
• 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/BanachFixpoint.glob
• 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/Zm.vo
• 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CRing_Homomorphisms.vo
• 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/OpenUnit.vo
• 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/coq_reals/Rsign.vo
• 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARSpeedTests.vo
• 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/StepFunctionMonad.glob
• 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/order/TotalOrder.glob
• 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/Compress.vo
• 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Zsec.glob
• 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/RX_deg.vo
• 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Derivative.glob
• 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/MultivariatePolynomials.v
• 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CSumsReals.vo
• 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Qinf.vo
• 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/CPseudoMSpaces.vo
• 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/DiffTactics3.vo
• 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/complex/Complex_Exponential.glob
• 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/iso_CReals.v
• 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARtrans.vo
• 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/FTA.vo
• 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRball.vo
• 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CMetricFields.vo
• 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/CPoly_Shift.vo
• 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRtrans.vo
• 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/IntervalFunct.vo
• 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Integral.v
• 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARQ.vo
• 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/ProductMetric.glob
• 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/totalorder/ZMinMax.glob
• 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ApproximateRationals.glob
• 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/totalorder/ZMinMax.vo
• 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/Stability.vo
• 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/FTA.glob
• 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRIR.glob
• 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/totalorder/QMinMax.vo
• 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ACarith.glob
• 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/uneven_CRplus.vo
• 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Cesaro.glob
• 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/IrrCrit.glob
• 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/QnonNeg.vo
• 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/ModulusDerivative.glob
• 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRpi.vo
• 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/PartFunEquality.glob
• 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRArith_alg.vo
• 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/RasterQ.glob
• 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/order/PartialOrder.vo
• 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/StepQsec.glob
• 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/ZGcd.v
• 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/CPoly_Shift.glob
• 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Hausdorff.vo
• 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRcos.glob
• 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/RealFuncts.vo
• 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/IrrCrit.vo
• 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Qsec.vo
• 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/PartInterval.vo
• 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/complex/NRootCC.v
• 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/OddPolyRootIR.glob
• 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSemiGroups.vo
• 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARinterval.vo
• 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/rings/CRring.vo
• 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/RealCount.glob
• 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/MoreIntervals.v
• 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/order/TotalOrder.vo
• 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum.v
• 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/RX_div.vo
• 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/RefSeparating.v
• 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Metric.vo
• 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/nat_Q_lists.vo
• 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/CompleteProduct.vo
• 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/ordfields/CRordfield.vo
• 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRsign.vo
• 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARarctan_small.glob
• 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/CPoly_Contin1.vo
• 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/List.vo
• 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/reals/CRreal.glob
• 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/Zlcm.vo
• 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/RSetoid.vo
• 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/RealLists.glob
• 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Cesaro.vo
• 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRroot.v
• 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/QX_ZX.glob
• 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/Q_can.vo
• 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/CPoly_Euclid.glob
• 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/PosSeq.vo
• 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/QnnInf.vo
• 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/fields/CRfield.vo
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/Exponential.v
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/CRgroup.vo
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRGeometricSum.v
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Series.v
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/IntegrationRules.glob
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Complete.v
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/CRsemigroup.vo
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/QposInf.vo
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/raster/Raster.vo
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/CC_Props.glob
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/CRsetoid.vo
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Classified.v
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/CLogic.v
• 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/CRmonoid.vo
• 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/FromMetric2.glob
• 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/decsetoid.vo
• 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/InvTrigonom.v
• 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Qgcd.vo
• 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/lattice/CRlattice.vo
• 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/OperationClasses.vo
• 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/CRabgroup.vo
• 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/PowerBound.vo
• 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CPoly_Contin.vo
• 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/COrdFields.v
• 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARsign.vo
• 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Zsec.vo
• 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARArith.v
• 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/metric.v
• 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/Integration.v
• 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/FieldReflection.v
• 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/QX_extract_roots.glob
• 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/IntegrableFunction.vo
• 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Differentiability.glob
• 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Bridges_iso.v
• 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Max_AbsIR.v
• 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/MoreFunctions.v
• 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/RefLemma.v
• 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Qpossetoid.vo
• 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/BoundedFunction.vo
• 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Qsums.glob
• 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/classes/Qposclasses.vo
• 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/Prod_Sub.glob
• 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/Zm.glob
• 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/Compress.glob
• 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Ranges.vo
• 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/Cmod.vo
• 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/LinfMetric.glob
• 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/Cauchy_COF.v
• 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/Picard.v
• 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARarctan.glob
• 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CRings.v
• 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/CRmetric.vo
• 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Qpossec.glob
• 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/rings/Qring.vo
• 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/CRingClass.vo
• 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/OperationClasses.glob
• 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Nsec.vo
• 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/FunctSequence.v
• 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRexp.v
• 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Continuity.v
• 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/FinEnum.v
• 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/order/SemiLattice.vo
• 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Hausdorff.glob
• 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_freem.vo
• 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Intervals.v
• 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/RingReflection.v
• 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/partialorder/CRpartialorder.vo
• 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/MoreFunSeries.v
• 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Bridges_LUB.v
• 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/classes/Qclasses.vo
• 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/UniformContinuity.glob
• 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRconst.vo
• 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Zfinsetoid.vo
• 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/SimpleIntegration.v
• 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Composition.v
• 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/ordfields/Qordfield.vo
• 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/Pi.v
• 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/QSposmonoid.vo
• 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Nfinsetoid.vo
• 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/Z.vo
• 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSetoids.v
• 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/QSposgroup.vo
• 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Nsetoid.vo
• 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRcorrect.v
• 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/Qposgroup.vo
• 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/AQmetric.glob
• 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_cycm.vo
• 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/SetoidPermutation.vo
• 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CAbMonoids.vo
• 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Qposmonoid.vo
• 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/Zlcm.glob
• 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CReals.vo
• 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/coq_reals/Rreals.glob
• 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSetoidInc.vo
• 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/QSposabgroup.vo
• 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/Qposabgroup.vo
• 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CSumsReals.glob
• 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/Rational.vo
• 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Qsec.glob
• 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Qsetoid.vo
• 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/Qauto.vo
• 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/COrdFields2.v
• 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/DiffTactics2.glob
• 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Zsetoid.vo
• 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRsin.v
• 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Npossetoid.vo
• 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/QnonNeg.glob
• 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/RefSeparated.v
• 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/reals/Cauchy_IR.vo
• 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CauchySeq.v
• 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Cauchy_CReals.v
• 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Qpossemigroup.vo
• 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/freem_to_Nm.vo
• 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/QSpossemigroup.vo
• 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/StepFunction.v
• 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/order/Lattice.vo
• 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/fields/Qfield.vo
• 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/TaylorLemma.v
• 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSetoidFun.v
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Qmonoid.vo
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Zmonoid.vo
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRstreams.v
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CMetricFields.glob
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/CPoly_Contin1.glob
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/Qgroup.vo
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/CalculusTheorems.v
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/UCFnMonoid.vo
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/rings/Zring.vo
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Npossec.vo
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/StepFunctionSetoid.v
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Nmonoid.vo
• 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Nposmonoid.vo
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CornScope.vo
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/coq_reals/Rreals_iso.v
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/FunctSeries.v
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CRing_as_Ring.vo
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/TrigMon.v
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Metric.glob
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Partitions.v
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/Qabgroup.vo
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Npossemigroup.vo
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/Zgroup.vo
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/LocatedSubset.glob
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/ZDivides.v
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARabs.glob
• 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Q_in_CReals.v
• 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/Zabgroup.vo
• 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/list_separates.vo
• 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Classification.vo
• 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/ContinuousCorrect.glob
• 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CRing_Homomorphisms.glob
• 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/raster/Raster.glob
• 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/RX_deg.glob
• 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Nsemigroup.vo
• 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Qsemigroup.vo
• 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/NRootIR.v
• 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSums.v
• 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Zsemigroup.vo
• 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRGroupOps.v
• 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/Interval.v
• 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/COrdCauchy.v
• 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSemiGroups.glob
• 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/PosSeq.glob
• 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/RefSepRef.v
• 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Rolle.v
• 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CFields.v
• 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Q_dense.v
• 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CMonoids.v
• 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/CornBasics.v
• 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/CPseudoMSpaces.glob
• 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/IntervalFunct.glob
• 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/order/PartialOrder.glob
• 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/MoreIntegrals.v
• 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/TaylorSeries.v
• 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRpower.v
• 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/rings/CRring.glob
• 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/ZBasics.v
• 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/NthDerivative.v
• 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/nat_Q_lists.glob
• 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/PointFree.vo
• 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/DerivativeOps.v
• 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Prelength.v
• 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/Expon.v
• 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Graph.v
• 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/Trigonometric.v
• 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPoly_Degree.v
• 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/complex/CComplex.v
• 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/FTC.v
• 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRball.glob
• 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/RealPowers.v
• 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/CMetricSpaces.v
• 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/RasterizeQ.v
• 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARroot.v
• 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/StrongIVT.v
• 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/WeakIVTQ.glob
• 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/DistanceMetricSpace.glob
• 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/order/Lattice.glob
• 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/CPMSTheory.v
• 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/RingClass.glob
• 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/MoreArcTan.v
• 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/ZMod.v
• 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/WeakIVT.v
• 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/KneserLemma.v
• 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/OpenUnit.glob
• 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/order/SemiLattice.glob
• 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/Pair.vo
• 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARpi.glob
• 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARAlternatingSum.v
• 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/Bernstein.v
• 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPoly_ApZero.v
• 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/lattice/CRlattice.glob
• 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/Q_can.glob
• 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/COrdLemmas.v
• 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/Classic.vo
• 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPoly_Newton.v
• 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/PowerSeries.v
• 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/RSetoid.glob
• 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/ContFunctions.v
• 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/Stability.glob
• 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/totalorder/QposMinMax.v
• 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/AlgReflection.v
• 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/PartInterval.glob
• 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/FTAreg.v
• 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/IVT.v
• 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/LazyNat.vo
• 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/COrdAbs.v
• 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/MainLemma.v
• 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/FunctSums.v
• 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/Z.glob
• 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/List.glob
• 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/ArTanH.v
• 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/L1metric.v
• 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/LinfMetricMonad.v
• 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARbigQ.glob
• 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/NNUpperR.v
• 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Hausdorff.v
• 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/complex/AbsCC.v
• 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/Q.v
• 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/Liouville.v
• 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CReals1.v
• 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRAlternatingSum_alg.v
• 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/PartFunEquality.v
• 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/Qmetric.v
• 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CAbGroups.v
• 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRartanh_slow.v
• 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/uneven_CRplus.glob
• 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CGroups.v
• 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/SetoidPermutation.glob
• 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/CompleteProduct.glob
• 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/Equiv.v
• 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Taylor.v
• 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/Plot.v
• 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/P.vo
• 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/Zm.v
• 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/R_morphism.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/CPoly_Rev.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/IR_CPMSpace.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Limit.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/PowerBound.glob
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARplot.glob
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/LipExt.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/QnnInf.glob
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRln.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/KeyLemma.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARsin.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRarctan_small.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/DiffTactics3.glob
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Container.vo
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CPoly_NthCoeff.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/QX_root_loc.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/ProductMetric.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Derivative.v
• 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/RealLists.v
• 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/StepFunctionMonad.v
• 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/MetricMorphisms.v
• 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/QX_ZX.v
• 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRpi_fast.v
• 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/DiffTactics2.v
• 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRarctan.v
• 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARcos.glob
• 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/LinfDistMonad.v
• 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARexp.v
• 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/QposInf.glob
• 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Nsetoid.glob
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRabs.v
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Qgcd.glob
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/Classic.glob
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/coq_reals/Rreals.v
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/RealFuncts.glob
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/Differentiability.v
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/rings/Qring.glob
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/RasterQ.v
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Nsec.glob
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRIR.v
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Qpossec.v
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/transc/SinCos.v
• 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRpi_slow.v
• 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/totalorder/QMinMax.v
• 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/N.vo
• 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARbigD.v
• 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CPoly_Contin.glob
• 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/Prod_Sub.v
• 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/IntegrationRules.v
• 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/LinfMetric.v
• 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/StepQsec.v
• 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Qdlog.v
• 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/order/TotalOrder.v
• 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/FromMetric2.v
• 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/UniformContinuity.v
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/Pair.glob
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/ModulusDerivative.v
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRsum.v
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/ordfields/CRordfield.glob
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/decsetoid.glob
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/RealCount.v
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/QX_extract_roots.v
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRcos.v
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/CRsemigroup.glob
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/totalorder/ZMinMax.v
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Zsec.v
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/fields/CRfield.glob
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/IrrCrit.v
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/LocatedSubset.v
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Qsec.v
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/Cmod.glob
• 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/OddPolyRootIR.v
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/PointFree.glob
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSemiGroups.v
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ode/BanachFixpoint.v
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSetoidInc.glob
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/CPoly_Euclid.v
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/CC_Props.v
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ApproximateRationals.v
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/CRgroup.glob
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/complex/Complex_Exponential.v
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/FTA.v
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/RealFuncts.v
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARQ.glob
• 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metrics/CPseudoMSpaces.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/Zlcm.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/reals/CRreal.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/Cesaro.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Metric.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/IntervalFunct.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/lattice/CRlattice.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/RX_deg.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Qinf.glob
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Zsetoid.glob
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/Compress.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/LazyNat.glob
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Qsums.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRArith_alg.glob
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/list_separates.glob
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/QnonNeg.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/raster/Raster.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/CornTac.vo
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/CPoly_Shift.v
• 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/PartInterval.v
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/OperationClasses.v
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Qsetoid.glob
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/OpenUnit.v
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_cycm.glob
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARarctan_small.v
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARinterval.glob
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/nat_Q_lists.v
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Npossec.glob
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/ContinuousCorrect.v
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/AQmetric.v
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARarctan.v
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CSumsReals.v
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ACarith.v
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/RSetoid.v
• 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/DiffTactics3.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Nsetoid.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/RingClass.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CRing_Homomorphisms.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Qpossetoid.glob
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/ftc/WeakIVTQ.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/order/PartialOrder.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/Q_can.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARabs.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/QposInf.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Zfinsetoid.glob
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/DistanceMetricSpace.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/fta/CPoly_Contin1.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/order/Lattice.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/PosSeq.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Nfinsetoid.glob
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/rings/CRring.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/CRmonoid.glob
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/RX_div.glob
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/CompleteProduct.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CMetricFields.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CAbMonoids.glob
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/order/SemiLattice.v
• 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Nsec.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/P.glob
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/PowerBound.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/CRingClass.glob
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Zsetoid.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CPoly_Contin.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/Classic.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Npossetoid.glob
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Ranges.glob
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Qpossetoid.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/Stability.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_freem.glob
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/List.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Extract.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/ordfields/CRordfield.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Qsetoid.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARbigQ.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/SetoidPermutation.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/CRsetoid.glob
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/LazyNat.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRball.v
• 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/rings/Qring.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/Z.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CSetoidInc.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/ordfields/Qordfield.glob
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRsign.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/Zmod/Cmod.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/fields/CRfield.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRArith_alg.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/uneven_CRplus.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/PointFree.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/QnnInf.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Npossetoid.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/CRsemigroup.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Zmonoid.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_freem.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/Step.vo
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/CRabgroup.glob
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Zfinsetoid.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/decsetoid.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/CRgroup.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CAbMonoids.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Zmonoid.glob
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARplot.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/classes/Qclasses.glob
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/Nfinsetoid.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Classification.glob
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Qgcd.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARcos.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARpi.v
• 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Nm_to_cycm.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/CRingClass.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Qmonoid.glob
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Qinf.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Qmonoid.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/CRmetric.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/PropDecid.vo
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/structures/Npossec.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/setoids/CRsetoid.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Nmonoid.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CReals.glob
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/CRmonoid.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARQ.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/Rational.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/liouville/RX_div.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Nmonoid.glob
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Npossemigroup.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/UCFnMonoid.glob
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/DiffTactics1.vo
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/ordfields/Qordfield.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRconst.glob
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARinterval.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/freem_to_Nm.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/CReals.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Classification.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Nposmonoid.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Zsemigroup.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/CRmetric.glob
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/QSposmonoid.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/Qauto.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/CornTac.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/classes/Qposclasses.glob
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/IntegrableFunction.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/CRabgroup.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Qposmonoid.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/rings/Zring.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Nsemigroup.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/Rational.glob
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/QSposgroup.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/PropDecid.glob
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/QSposabgroup.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/Zgroup.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/BoundedFunction.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRsign.glob
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Qsemigroup.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/partialorder/CRpartialorder.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/fields/Qfield.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/Zabgroup.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/Qgroup.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/list_separates.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/Qposgroup.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/freem_to_Nm.glob
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/Qabgroup.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRtrans.v
• 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/reals/Cauchy_IR.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/Qposabgroup.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/IntegrableFunction.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/QSpossemigroup.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Zsemigroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/DiffTactics1.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Qpossemigroup.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Nposmonoid.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARsign.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/Step.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CornScope.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/partialorder/CRpartialorder.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/P.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Npossemigroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/QSposmonoid.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/monoids/Qposmonoid.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/Pair.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Nsemigroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/rings/Zring.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CornScope.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CRing_as_Ring.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/Qgroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/logic/PropDecid.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/UCFnMonoid.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARsign.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/metric2/BoundedFunction.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRconst.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/coq_reals/Rsign.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/coq_reals/Rsign.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/Zgroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARSpeedTests.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/Qposgroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/Qauto.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/fields/Qfield.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Container.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/groups/QSposgroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/Qabgroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/Zabgroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Qsemigroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/metric2/Ranges.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Extract.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRpi.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/classes/Qclasses.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/classes/Qposclasses.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/QSposabgroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/abgroups/Qposabgroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRtrans.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/N.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/Qpossemigroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/fast/CRpi.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/semigroups/QSpossemigroup.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARSpeedTests.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/CornTac.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARtrans.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/model/reals/Cauchy_IR.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/reals/faster/ARtrans.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/util/Container.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/algebra/CRing_as_Ring.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/stdlib_omissions/N.v
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/DiffTactics1.glob
• 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/CoRN/tactics/Step.glob

Uninstall 🧹

Command

opam remove -y coq-corn.8.16.0

Return code

0

Missing removes

none

Wrong removes

none