« Up

library-fol 1.0+8.18 6 m 0 s 🏆

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-domains          base
base-nnp              base        Naked pointers prohibited in the OCaml heap
base-threads          base
base-unix             base
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   8.18.0      The Coq Proof Assistant
coq-core              8.18.0      The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            8.18.0      The Coq Proof Assistant -- Standard Library
coqide-server         8.18.0      The Coq Proof Assistant, XML protocol server
dune                  3.13.0      Fast, portable, and opinionated build system
ocaml                 5.0.0       The OCaml compiler (virtual package)
ocaml-base-compiler   5.0.0       Official release 5.0.0
ocaml-config          3           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"
version: "1.0+8.18"
maintainer: "kirst@cs.uni-saarland.de"
homepage: "https://github.com/uds-psl/coq-library-fol/"
dev-repo: "git+https://github.com/uds-psl/coq-library-fol/"
bug-reports: "https://github.com/uds-psl/coq-library-fol/issues"
authors: [
  "Dominik Kirst"
  "Johannes Hostert"
  "Andrej Dudenhefner"
  "Yannick Forster"
  "Marc Hermes"
  "Mark Koch"
  "Dominique Larchey-Wendling"
  "Niklas Mück"
  "Benjamin Peters"
  "Gert Smolka"
  "Dominik Wehr"
]
license: "MIT"
build: [
  [make "-j%{jobs}%"]
]
install: [
  [make "install"]
]
depends: [
  "coq" {>= "8.18" & < "8.19~"}
  "coq-library-undecidability" {= "1.1.1+8.18"}
]
synopsis: "A Coq Library for First-Order Logic"
url {
  src: "https://github.com/uds-psl/coq-library-fol/archive/refs/tags/v1.0+8.18.tar.gz"
  checksum: "sha256=9be91c51601e2a6afba5f71d44bdd1a5775345d2140c3a401d7c26ff58ad6351"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-library-fol.1.0+8.18 coq.8.18.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-library-fol.1.0+8.18 coq.8.18.0
Return code
0
Duration
19 m 0 s

Install 🚀

Command
opam list; echo; timeout 4h opam install -y -v coq-library-fol.1.0+8.18 coq.8.18.0
Return code
0
Duration
6 m 0 s

Installation size

Total: 17 M

  • 3 M ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/DemoMinZF.vo
  • 1 M ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/qdec.vo
  • 589 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Reification/GeneralReflection.vo
  • 564 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/ProofMode.vo
  • 495 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/ctq.vo
  • 439 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/DemoZF.vo
  • 408 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/DemoPA.vo
  • 403 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/HA_insep.vo
  • 386 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Semantics/Heyting/Heyting.vo
  • 301 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/bin_qdec.vo
  • 296 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Utils/PrenexNormalForm.glob
  • 253 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Reification/GeneralReflection.glob
  • 236 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Peano.glob
  • 235 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Peano.vo
  • 230 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/ArithmeticalHierarchy/ArithmeticalHierarchySemantic.glob
  • 223 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/sigma1.vo
  • 213 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/ProofMode.glob
  • 196 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Reification/DemoPAExtensional.vo
  • 187 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Coding.vo
  • 175 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/fol_utils.vo
  • 174 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Utils/PrenexNormalForm.vo
  • 174 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/Axiomatisations.vo
  • 172 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/ctq.glob
  • 159 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Tennenbaum_insep.vo
  • 158 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/ArithmeticalHierarchy/ArithmeticalHierarchySemantic.vo
  • 154 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/weak_strong.vo
  • 152 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Deduction/FragmentSequentFacts.vo
  • 152 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Variants.vo
  • 148 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Reification/DemoPA.vo
  • 145 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/TarskiCompleteness.vo
  • 144 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/NumberUtils.vo
  • 134 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/epf_mu.vo
  • 133 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/KripkeCompleteness.vo
  • 132 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/TarskiConstructions.vo
  • 132 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Semantics/Heyting/Soundness.vo
  • 128 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Coding.glob
  • 125 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/ArithmeticalHierarchy/ArithmeticalHierarchySyntactic.vo
  • 124 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/Abstract.vo
  • 122 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/TarskiCompleteness.glob
  • 117 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/qdec.glob
  • 115 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/Axiomatisations.glob
  • 110 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Tennenbaum_diagonal.vo
  • 99 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/HeytingCompleteness.vo
  • 98 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Church.vo
  • 97 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/KripkeCompleteness.glob
  • 97 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/HeytingMacNeille.vo
  • 96 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/TarskiConstructions.glob
  • 96 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/utils.vo
  • 92 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/PA_incompleteness.vo
  • 89 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/fol_incompleteness.vo
  • 87 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/ArithmeticalHierarchy/ArithmeticalHierarchySyntactic.glob
  • 83 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Semantics/Heyting/Soundness.glob
  • 82 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Formulas.vo
  • 81 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Deduction/FullSequentFacts.vo
  • 81 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/ProofMode.v
  • 78 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/Theories.vo
  • 73 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/HeytingCompleteness.glob
  • 67 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/ArithmeticalHierarchy/ArithmeticalHierarchyEquiv.vo
  • 67 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/weak_strong.glob
  • 65 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Tennenbaum_insep.glob
  • 64 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Deduction/FragmentSequentFacts.glob
  • 63 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/NumberUtils.glob
  • 61 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/EnumerationUtils.vo
  • 60 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/DemoPA.glob
  • 59 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Deduction/FullSequentFacts.glob
  • 58 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Reification/GeneralReflection.v
  • 56 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/MoreDecidabilityFacts.vo
  • 55 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/SyntheticInType.vo
  • 54 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Variants.glob
  • 51 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/HA_insep.glob
  • 47 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/Abstract.glob
  • 47 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/epf.vo
  • 45 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Deduction/FullSequent.vo
  • 43 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/sigma1.glob
  • 43 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/Theories.glob
  • 42 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Semantics/Heyting/Heyting.glob
  • 42 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/HeytingMacNeille.glob
  • 41 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/Hoas.vo
  • 40 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Reification/DemoPA.glob
  • 40 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/abstract_incompleteness.vo
  • 39 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/epf_mu.glob
  • 39 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Utils/MPFacts.vo
  • 38 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Deduction/FragmentSequent.vo
  • 38 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/SyntheticInType.glob
  • 38 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/CantorPairing.vo
  • 38 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Reification/DemoPAExtensional.glob
  • 38 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Tennenbaum_diagonal.glob
  • 38 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Peano.v
  • 36 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/StringToIdent.vo
  • 36 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/Consistency.vo
  • 34 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/formal_systems.vo
  • 33 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/ArithmeticalHierarchy/ArithmeticalHierarchyEquiv.glob
  • 30 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Sets.vo
  • 30 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/FiniteSets.vo
  • 30 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/fol_incompleteness.glob
  • 29 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Abstract_coding.vo
  • 29 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Church.glob
  • 28 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/DemoZF.glob
  • 28 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/PA_incompleteness.glob
  • 28 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/bin_qdec.glob
  • 26 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/ArithmeticalHierarchy/ArithmeticalHierarchySemantic.v
  • 26 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/TarskiCompleteness.v
  • 25 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/DemoMinZF.glob
  • 24 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/Axiomatisations.v
  • 24 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/qdec.v
  • 24 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Arithmetics.vo
  • 24 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/FullSyntax.vo
  • 23 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/FragmentSyntax.vo
  • 23 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/utils.glob
  • 21 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Theories.vo
  • 21 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/ctq.v
  • 20 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/abstract_incompleteness.glob
  • 19 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Utils/PrenexNormalForm.v
  • 19 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/KripkeCompleteness.v
  • 18 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Coding.v
  • 17 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/epf.glob
  • 17 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/TarskiConstructions.v
  • 17 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/EnumerationUtils.glob
  • 16 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/Consistency.glob
  • 15 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/ArithmeticalHierarchy/ArithmeticalHierarchySyntactic.v
  • 15 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/MoreDecidabilityFacts.glob
  • 15 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Deduction/FullSequent.glob
  • 14 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Utils/MPFacts.glob
  • 14 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Tennenbaum_insep.v
  • 13 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/CantorPairing.glob
  • 13 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/fol_utils.glob
  • 12 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Variants.v
  • 12 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/formal_systems.glob
  • 12 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/HeytingCompleteness.v
  • 11 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Deduction/FragmentSequentFacts.v
  • 11 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/NumberUtils.v
  • 11 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/Abstract.v
  • 11 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/weak_strong.v
  • 10 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Formulas.glob
  • 10 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/sigma1.v
  • 10 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Deduction/FragmentSequent.glob
  • 10 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/epf_mu.v
  • 9 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/Hoas.glob
  • 9 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Deduction/FullSequentFacts.v
  • 9 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/HeytingMacNeille.v
  • 9 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Tennenbaum_diagonal.v
  • 9 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Semantics/Heyting/Heyting.v
  • 9 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/DemoMinZF.v
  • 9 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/DemoPA.v
  • 8 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/HA_insep.v
  • 8 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Abstract_coding.glob
  • 8 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/Theories.v
  • 8 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/SyntheticInType.v
  • 7 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Reification/DemoPAExtensional.v
  • 7 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Reification/DemoPA.v
  • 7 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/DN_Utils.vo
  • 6 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/utils.v
  • 6 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/DemoZF.v
  • 6 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/PA_incompleteness.v
  • 6 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Semantics/Heyting/Soundness.v
  • 5 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Church.v
  • 5 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/epf.v
  • 5 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/fol_incompleteness.v
  • 5 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/ArithmeticalHierarchy/ArithmeticalHierarchyEquiv.v
  • 5 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/abstract_incompleteness.v
  • 5 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/EnumerationUtils.v
  • 5 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/bin_qdec.v
  • 4 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/fol_utils.v
  • 4 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/DN_Utils.glob
  • 3 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/MoreDecidabilityFacts.v
  • 3 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Completeness/Consistency.v
  • 3 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Utils/MPFacts.v
  • 3 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/Hoas.v
  • 3 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Incompleteness/formal_systems.v
  • 2 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Formulas.v
  • 2 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/CantorPairing.v
  • 2 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Deduction/FragmentSequent.v
  • 2 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/Abstract_coding.v
  • 2 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Deduction/FullSequent.v
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/StringToIdent.glob
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Tennenbaum/DN_Utils.v
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Proofmode/StringToIdent.v
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Sets.glob
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Arithmetics.glob
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/FiniteSets.glob
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Sets.v
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/FragmentSyntax.glob
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/FiniteSets.v
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/FullSyntax.glob
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Arithmetics.v
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Theories.glob
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/FragmentSyntax.v
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/FullSyntax.v
  • 1 K ../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/FOL/Theories.v

Uninstall 🧹

Command
opam remove -y coq-library-fol.1.0+8.18
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣