« Up

num-analysis 1.0.0 3 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.16.1      Formal proof management system
dune                  3.12.1      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"
synopsis: "Numerical Analysis in Coq"
maintainer: "MILC project <milc@inria.fr>"
authors: [ "Sylvie Boldo" "François Clément" "Vincent Martin" "Micaela Mayero" "Florian Faissole" "Houda Mouhcine" "Louise Leclerc" "Stéphane Aubry" ]
homepage: "https://lipn.univ-paris13.fr/coq-num-analysis/"
dev-repo: "git+https://lipn.univ-paris13.fr/coq-num-analysis/"
bug-reports: "https://lipn.univ-paris13.fr/coq-num-analysis/issues"
license: "LGPL-3.0-or-later"
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
  "coq" {>= "8.15.0"}
  "coq-mathcomp-ssreflect" {>= "1.15.0"}
  "coq-coquelicot" {= "3.2.0"}
  "coq-flocq" {>= "4.1.0"}
]
tags: [
  "category:Mathematics/Real Calculus and Topology"
  "keyword:real analysis"
  "keyword:Lax-Milgram theorem"
  "keyword:Lebesgue integration"
  "keyword:Tonelli theorem"
  "keyword:Bochner integration"
  "logpath:Lebesgue"
  "logpath:LM"
  "date:2022-09-06"
]
url {
  src: "https://depot.lipn.univ-paris13.fr/mayero/coq-num-analysis/-/archive/1.0/coq-num-analysis-1.0.tar.gz"
  checksum: "sha256=c230cb37b61e3b9de8619b66e470981ba986a4009c6e9dda0d3958d0858df40a"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-num-analysis.1.0.0 coq.8.16.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-num-analysis.1.0.0 coq.8.16.1
Return code
0
Duration
4 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-num-analysis.1.0.0 coq.8.16.1
Return code
0
Duration
3 m 0 s

Installation size

Total: 14 M

  • 537 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/Bi_fun.vo
  • 468 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/Bi_fun.glob
  • 390 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/lax_milgram.glob
  • 346 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/simpl_fun.vo
  • 341 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Rbar_compl.vo
  • 302 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measure_R_compl.glob
  • 300 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Rbar_compl.glob
  • 299 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/hilbert.glob
  • 274 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset.vo
  • 261 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measure_R_compl.vo
  • 244 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/simple_fun.glob
  • 231 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/lax_milgram.vo
  • 222 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/LInt_p.glob
  • 221 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measure_R.glob
  • 219 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/simple_fun.vo
  • 206 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/continuous_linear_map.glob
  • 196 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_system.glob
  • 192 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/hilbert.vo
  • 182 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measurable_fun.glob
  • 180 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/BInt_sf.glob
  • 178 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/sigma_algebra_R_Rbar.glob
  • 171 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_finite.glob
  • 166 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/fixed_point.glob
  • 165 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/simpl_fun.glob
  • 165 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measure.glob
  • 164 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_system.vo
  • 162 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measure_R.vo
  • 161 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_finite.vo
  • 161 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/Bsf_Lsf.glob
  • 159 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Tonelli.glob
  • 156 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/LInt_p.vo
  • 155 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_seq.glob
  • 153 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset.glob
  • 150 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/sigma_algebra_R_Rbar.vo
  • 147 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/continuous_linear_map.vo
  • 145 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measurable_fun.vo
  • 140 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_seq.vo
  • 137 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/Bsf_Lsf.vo
  • 132 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/CUS_Lim_seq.glob
  • 130 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_system_base.vo
  • 129 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Tonelli.vo
  • 129 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_system_base.glob
  • 121 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/BInt_Bif.glob
  • 119 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measure.vo
  • 113 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/BInt_LInt_p.glob
  • 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/sum_Rbar_nonneg.glob
  • 109 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/sum_Rbar_nonneg.vo
  • 109 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/fixed_point.vo
  • 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/hierarchyD.vo
  • 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/BInt_sf.vo
  • 103 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/sort_compl.vo
  • 99 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/hierarchyD.glob
  • 94 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/R_compl.vo
  • 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/CUS_Lim_seq.vo
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/BInt_LInt_p.vo
  • 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/topo_bases_R.vo
  • 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measure_R_uniq_compl.glob
  • 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/BInt_Bif.vo
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/R_compl.glob
  • 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/countable_sets.vo
  • 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Rbar_compl.v
  • 77 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/Bi_fun.v
  • 74 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measure_R_uniq_compl.vo
  • 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/BInt_R.vo
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/LInt.vo
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/BInt_R.glob
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Mp.vo
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/sort_compl.glob
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/sigma_algebra.vo
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/topology_compl.vo
  • 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/topo_bases_R.glob
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/B_spaces.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/lax_milgram.v
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/linear_map.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/countable_sets.glob
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/R_compl.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/square_bij.vo
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measure_R_compl.v
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/sigma_algebra.glob
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/topology_compl.glob
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measurable.vo
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/UniformSpace_compl.vo
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/check_sub_structure.vo
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_system_gen.glob
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/FinBij.vo
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_system_gen.vo
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/lax_milgram_cea.vo
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/B_spaces.glob
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_system.v
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/hilbert.v
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/simple_fun.v
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/compatible.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_charac.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/LInt.glob
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/LInt_p.v
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measurable_fun.v
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/R_compl.glob
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/continuous_linear_map.v
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/simpl_fun.v
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/sigma_algebra_R_Rbar.v
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_finite.v
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/subset_compl.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_seq.v
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measure_R.v
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/FinBij.glob
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/series.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset.v
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/complete_normed_module_series.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/Bsf_Lsf.v
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Tonelli.v
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measure.v
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/Rmax_n.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/square_bij.glob
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/UniformSpace_compl.glob
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/linear_map.glob
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Mp.glob
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measurable.glob
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/hierarchy_notations.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/fixed_point.v
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_system_base.v
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/BInt_sf.v
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/list_compl.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_charac.glob
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/nat_compl.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/sum_Rbar_nonneg.v
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/compatible.glob
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/check_sub_structure.glob
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/subset_compl.glob
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/CUS_Lim_seq.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/hierarchyD.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/lax_milgram_cea.glob
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/logic_tricks.vo
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/BInt_LInt_p.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/LInt.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/BInt_Bif.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measure_R_uniq_compl.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/R_compl.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/topo_bases_R.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/sort_compl.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/logic_compl.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/sigma_algebra.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/list_compl.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_system_gen.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/topology_compl.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/BInt_R.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measurable.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/countable_sets.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/series.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/B_spaces.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/FinBij.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Mp.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/linear_map.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/logic_tricks.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/complete_normed_module_series.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/UniformSpace_compl.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/R_compl.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/square_bij.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/check_sub_structure.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/Subset_charac.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/compatible.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/subset_compl.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/lax_milgram_cea.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/nat_compl.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/Rmax_n.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/list_compl.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/LM/logic_tricks.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/series.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/complete_normed_module_series.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/nat_compl.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/logic_compl.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/Rmax_n.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measurable_R.vo
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/hierarchy_notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/logic_compl.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/bochner_integral/hierarchy_notations.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measurable_R.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Lebesgue/measurable_R.glob

Uninstall 🧹

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

Sources are on GitHub © Guillaume Claret 🐣