« Up

coqtail 8.18 2 m 0 s 🏆

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   8.17.0      The Coq Proof Assistant
coq-core              8.17.0      The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            8.17.0      The Coq Proof Assistant -- Standard Library
coqide-server         8.17.0      The Coq Proof Assistant, XML protocol server
dune                  3.13.0      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.6       A library manager for OCaml
zarith                1.13        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "palmskog@gmail.com"
homepage: "https://github.com/coq-community/coqtail-math"
dev-repo: "git+https://github.com/coq-community/coqtail-math.git"
bug-reports: "https://github.com/coq-community/coqtail-math/issues"
license: "LGPL-3.0-only"
synopsis: "Library of mathematical theorems and tools proved inside the Coq"
description: """
Coqtail is a library of mathematical theorems and tools proved inside
the Coq proof assistant. Results range mostly from arithmetic to real
and complex analysis."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
  "coq" {>= "8.11" & < "8.19"}
]
tags: [
  "category:Mathematics/Real Calculus and Topology"
  "keyword:real analysis"
  "keyword:complex analysis"
  "logpath:Coqtail"
  "date:2023-11-23"
]
authors: [
  "Guillaume Allais"
  "Sylvain Dailler"
  "Hugo Férée"
  "Jean-Marie Madiot"
  "Pierre-Marie Pédrot"
  "Amaury Pouly"
]
url {
  src: "https://github.com/coq-community/coqtail-math/archive/8.18.tar.gz"
  checksum: "sha512=e0dd64426ac5ba25603ed57d3908b533c9c674aba453178851ae14f95dac81bab56eb16a9302b7a29079596057353fed773b99076449d3cd132f2e0ef6c6c1f1"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-coqtail.8.18 coq.8.17.0
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; timeout 4h opam install -y --deps-only coq-coqtail.8.18 coq.8.17.0
Return code
0
Duration
1 m 0 s

Install 🚀

Command
opam list; echo; timeout 4h opam install -y -v coq-coqtail.8.18 coq.8.17.0
Return code
0
Duration
2 m 0 s

Installation size

Total: 20 M

  • 685 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Hopital.glob
  • 342 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Lagrange_four_square.vo
  • 333 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rzeta2.glob
  • 308 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_diff.glob
  • 302 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rzeta2.vo
  • 271 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Croot_n.vo
  • 245 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_cv_facts.glob
  • 230 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Hopital.vo
  • 214 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_facts.glob
  • 196 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Wallis.glob
  • 181 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cprop_base.vo
  • 181 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rel_facts.glob
  • 178 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_deriv.glob
  • 171 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/CFsequence_facts.glob
  • 170 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Ndiv.glob
  • 168 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_derivability.glob
  • 154 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_base_facts.glob
  • 152 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cprop_base.glob
  • 147 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Croot_n.glob
  • 146 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_cv_facts.glob
  • 144 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Ndiv.vo
  • 140 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rtactic.vo
  • 138 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_cv_facts.vo
  • 138 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Wallis.vo
  • 133 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rel_facts.vo
  • 133 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RFsequence_facts.glob
  • 132 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_facts.vo
  • 129 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/MillerRabin.vo
  • 128 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_diff.vo
  • 126 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRfunctions.vo
  • 126 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRfunctions.glob
  • 123 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis5.glob
  • 121 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative.glob
  • 119 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Lagrange_four_square.glob
  • 117 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cexp.glob
  • 116 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_facts.glob
  • 112 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_prop.vo
  • 112 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_usual.glob
  • 111 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_deriv.vo
  • 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral.glob
  • 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ratan.glob
  • 109 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Csequence_facts.glob
  • 109 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_facts.glob
  • 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/CFsequence_facts.vo
  • 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_base_facts.vo
  • 107 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_sums_facts.glob
  • 107 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cexp.vo
  • 107 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_usual_facts.vo
  • 105 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_usual_facts.glob
  • 104 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Hopital.v
  • 103 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Znumfacts.vo
  • 100 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_definition.vo
  • 99 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_usual.vo
  • 98 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_instance.vo
  • 98 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_derivability.vo
  • 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Riemann_integrable.glob
  • 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis5.vo
  • 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral.vo
  • 95 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_sums_facts.vo
  • 95 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def_simpl.glob
  • 95 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums_facts.glob
  • 94 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ratan.vo
  • 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_cv_facts.vo
  • 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_facts.vo
  • 91 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Reirr.vo
  • 90 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RStirling.vo
  • 88 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rinterval.glob
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/MillerRabin.glob
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_facts.vo
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cderiv.glob
  • 86 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cbase.vo
  • 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpow_plus.glob
  • 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Natsets.vo
  • 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RFsequence_facts.vo
  • 82 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rinterval.vo
  • 82 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_cv_facts.vo
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative.vo
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cmet.glob
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_quote.vo
  • 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpow_plus.vo
  • 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_facts.vo
  • 79 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Csequence_facts.vo
  • 79 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RTaylor.vo
  • 77 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/Evect.vo
  • 75 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Modulo.vo
  • 75 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Reirr.glob
  • 75 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Hierarchy/Commutative_ring_binomial.vo
  • 74 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Riemann_integrable.vo
  • 74 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_taylor.vo
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RStirling.glob
  • 71 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_radius_facts.glob
  • 70 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics_reflection.vo
  • 70 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cnorm.vo
  • 70 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_cv_facts.glob
  • 70 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cmet.vo
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rtactic.glob
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cderiv.vo
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_base_facts.vo
  • 68 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRIneq.glob
  • 68 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cnorm.glob
  • 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def_simpl.vo
  • 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_radius_facts.vo
  • 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpow_facts.vo
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Logic/Runcountable.vo
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_base_facts.glob
  • 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_monotonicity.glob
  • 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rtrigo_facts.vo
  • 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Logic/Runcountable.glob
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Logic/Rmarkov.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRIneq.vo
  • 60 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpow_facts.glob
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpolar.vo
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_RiemannInt.vo
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_subsequence.vo
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_RiemannInt.glob
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Hierarchy/Commutative_ring_binomial.glob
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Ztools.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Triangular.vo
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_base_facts.vo
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Logic/Rmarkov.glob
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums_facts.vo
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Cauchy_lipschitz.vo
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_monotonicity.vo
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Zlittle_fermat.vo
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_definition.glob
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_extend.vo
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_def.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_continuity.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rzeta2.v
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cfunctions.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_taylor.glob
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RTaylor.glob
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_facts.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_usual.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_remainder_facts.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_examples.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_basic_facts.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nlittle_fermat.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_def.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RIVT.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def_simpl.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_instance.glob
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_def.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rtrigo_facts.glob
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_usual.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nlittle_fermat.glob
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cseries_facts.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_facts.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nnewton.glob
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rewrite_facts.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_diff.v
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_def.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_def.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rextensionality.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Zprime.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_cont.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpow.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Finite_Calculus/Definitions.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_ring.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_base_facts.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_facts.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cbase.glob
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/realisation_by_stdlib.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_usual.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative_facts.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Ctacfield.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_cv_facts.v
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nbinomial.glob
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_usual.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nbinomial.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_facts.v
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/Evect.glob
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Ndiv.v
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_pos_facts.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def.glob
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_MVT.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_bound_facts.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_quote.glob
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/CFsequence.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cdefinitions.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Csequence_def.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyR_dist.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_prop.glob
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_facts.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_tactic.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_deriv.v
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_subsequence.glob
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_def.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cseries.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/integrales.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RFsequence.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rel_facts.v
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_facts.glob
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_base_facts.v
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_def.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries.vo
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Zeqm.vo
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Natsets.glob
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence.vo
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_def.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Csequence.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyNNR.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cprop_base.v
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_base_facts.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_continuity.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics_reflection.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nnewton.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nfinite_prod.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_def.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpolar.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nfinite_sum.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rewrite_facts.glob
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Cauchy_lipschitz.glob
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_derivability.v
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_stdlib.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Zpow.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyINR.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Znumfacts.glob
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Complex.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbasic_fun.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Wallis.v
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyReals.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbase.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRfunctions.v
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/Vectorial_Cauchy.vo
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_facts.glob
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/MyNat.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nfinite_sum.glob
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/CFsequence_facts.v
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Ztools.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cseries_facts.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis5.v
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_base_facts.glob
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cfunctions.glob
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def_simpl.glob
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Modulo.glob
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative.v
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_cv_facts.v
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_basic_facts.glob
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_usual.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Croot_n.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_def.glob
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ratan.v
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RIVT.glob
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/integrales.glob
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_remainder_facts.glob
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nk_ind.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_extend.glob
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Lagrange_four_square.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Ninductions.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_facts.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/MyZ.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nk_ind.glob
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Npow.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_def.glob
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RFsequence_facts.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_cont.glob
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rtactic.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_def.glob
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_usual_facts.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_facts.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/MillerRabin.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Zlittle_fermat.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_facts.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/PI.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Riemann_integrable.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_sums_facts.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cexp.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rinterval.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def_simpl.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_usual.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Csequence_facts.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_MVT.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nfinite_prod.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_facts.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rextensionality.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_usual.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_bound_facts.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nle.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_monotonicity.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Ntools.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cderiv.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_usual.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_radius_facts.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/realisation_by_stdlib.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nminus.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Reirr.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_def.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cmet.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_pos_facts.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Triangular.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Functions.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRIneq.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_def.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Finite_Calculus/Definitions.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RTaylor.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RStirling.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_base_facts.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cdefinitions.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Natsets.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_quote.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_instance.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Monad.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative_facts.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums_facts.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cnorm.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_examples.glob
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Zeqm.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Logic/Rmarkov.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Examples.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_cv_facts.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cbase.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Zpow.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Logic/Runcountable.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_RiemannInt.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Csequence_def.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_facts.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_subsequence.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_base_facts.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nbinomial.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpow.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_tactics_reflection.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpow_facts.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rtrigo_facts.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Examples.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_taylor.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Functions.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Modulo.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Hierarchy/Commutative_ring_binomial.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Znumfacts.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Hierarchy/Type_class_definition.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_prop.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpow_plus.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Npow.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyR_dist.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_extend.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Zprime.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_continuity.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Monad.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_def.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/CFsequence.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nk_ind.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_facts.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Monad/Option.vo
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Ztools.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Monad/Option.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RFsequence.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/Vectorial_Cauchy.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RIVT.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nlittle_fermat.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nfinite_sum.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_rewrite_facts.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpolar.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cfunctions.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_def.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_ring.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_def.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_cont.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/PI.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cseries_facts.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/Evect.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_def.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Canalysis_basic_facts.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nnewton.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_usual.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Choice_facts.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def_simpl.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_facts.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_usual.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nfinite_prod.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_sums.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_base_facts.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Cauchy_lipschitz.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_facts.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_def.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/MyNeq.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Ctacfield.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/MyNat.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_def.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Choice_facts.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Triangular.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Zlittle_fermat.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_def.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_usual.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_remainder_facts.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/realisation_by_stdlib.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_def.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Hurwitz_def.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_MVT.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cdefinitions.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rextensionality.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_facts.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cseries.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Ninductions.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/InhabitedTactics.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_pos_facts.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Npow.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/integrales.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_usual.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Csequence_def.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_ring.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpow.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_bound_facts.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_derivative_facts.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_tactic.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/CFsequence.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Zprime.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_facts.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/RFsequence.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rintegral/Rintegral_tactic.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Dequa/Dequa_examples.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Ctacfield.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Zpow.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser/Rpser_def.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Finite_Calculus/Definitions.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Zeqm.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Tactics.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Examples.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Functions.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes_def.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cpser_def.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries/Rseries_def.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Ranalysis_usual.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Monad.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_def.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Cseries.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/PI.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Monad/Option.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyR_dist.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nle.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Ntools.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/MyNat.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Complex.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/MyZ.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Nth_derivative_def.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbasic_fun.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Ntools.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nminus.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbase.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyReals.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nle.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyNNR.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_stdlib.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ediff/Vectorial_Cauchy.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/Choice_facts.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyINR.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/MyNeq.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbasic_fun.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Ninductions.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/InhabitedTactics.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rpser.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Fresh/Inhabited/InhabitedTactics.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Complex.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rsequence/Rsequence_stdlib.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/MyZ.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyNNR.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyINR.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Rseries.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyReals.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/myReals/MyRbase.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Csequence.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Arith/Nminus.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/mytheories/MyNeq.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Ranalysis/Rfunction_classes.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Tactics.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Reals/Tactics.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Coqtail/Complex/Csequence.v

Uninstall 🧹

Command
opam remove -y coq-coqtail.8.18
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣