(2021-04-12 22:56:58 UTC)
# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils coq 8.11.1 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.10.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.10.1 Official release 4.10.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.1 A library manager for OCaml # opam file: opam-version: "2.0" authors: [ "Matthieu Sozeau <matthieu.sozeau@inria.fr>" "Cyprien Mangin <cyprien.mangin@m4x.org>" ] dev-repo: "git+https://github.com/mattam82/Coq-Equations.git#8.11" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://mattam82.github.io/Coq-Equations" bug-reports: "https://github.com/mattam82/Coq-Equations/issues" license: "LGPL-2.1-or-later" synopsis: "A function definition package for Coq" description: """ Equations is a function definition plugin for Coq, that allows the definition of functions by dependent pattern-matching and well-founded, mutual or nested structural recursion and compiles them into core terms. It automatically derives the clauses equations, the graph of the function and its associated elimination principle. """ tags: [ "keyword:dependent pattern-matching" "keyword:functional elimination" "category:Miscellaneous/Coq Extensions" "logpath:Equations" ] build: [ ["./configure.sh"] [make "-j%{jobs}%"] ] install: [ [make "install"] ] run-test: [ [make "test-suite"] ] depends: [ "coq" {>= "8.11~" & < "8.12~"} ] url { src: "https://github.com/mattam82/Coq-Equations/archive/v1.2.2-8.11.tar.gz" checksum: "sha512=6618338b365c7df36cfbc33aec8142dd51f24ddeebf36ca4cc4eb5148828e67dfe1f61cb9eb85d3b336346533c1e01c3fbd9f194a5652bb0771b5faeaff85deb" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-equations.1.2.2+8.11 coq.8.11.1
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y --deps-only coq-equations.1.2.2+8.11 coq.8.11.1
opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-equations.1.2.2+8.11 coq.8.11.1
Total: 5 M
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/equations_plugin.cmxs
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Telescopes.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Telescopes.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/equations_plugin.cmxa
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/NoConfusion.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/DepElim.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/DepElim.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/NoConfusion.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/DepElim.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/EqDec.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/EqDecInstances.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Relation.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/DepElim.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/EqDec.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Subterm.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Equations.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/EqDecInstances.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Relation_Properties.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/equations_common.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/EqDec.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/WellFoundedInstances.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Telescopes.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Telescopes.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/All.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Relation.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/EqDec.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Relation_Properties.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/DepElim.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/DepElim.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/equations_common.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/FunctionalInduction.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Tactics.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/FunctionalInduction.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Logic.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Subterm.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Classes.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Subterm.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/CoreTactics.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/splitting.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/covering.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Classes.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Loader.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/WellFounded.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/context_map.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/g_equations.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/principles.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Subterm.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/syntax.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/splitting.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/simplify.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/context_map.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/principles.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Tactics.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Init.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/sigma_types.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/covering.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/WellFounded.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Relation_Properties.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/g_equations.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Logic.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/principles_proofs.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Subterm.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/principles_proofs.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Classes.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/WellFoundedInstances.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/EqDec.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/syntax.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Classes.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/sigma_types.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Subterm.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/simplify.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/depelim.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/EqDec.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/depelim.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Telescopes.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Telescopes.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Constants.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/equations.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/equations.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Loader.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Constants.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/eqdec.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/FunctionalInduction.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/noconf_hom.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/FunctionalInduction.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Relation.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/subterm.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/CoreTactics.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/eqdec.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/noconf.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Init.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/extra_tactics.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/ederive.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Classes.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Logic.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Tactics.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Classes.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/EqDecInstances.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/noconf_hom.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/FunctionalInduction.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Tactics.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Signature.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/WellFounded.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Tactics.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/FunctionalInduction.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/equations_plugin_mod.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/equations_plugin_mod.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/ederive.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Constants.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Logic.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Constants.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/noconf.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/FunctionalExtensionality.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/extra_tactics.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/EqDecInstances.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/subterm.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Logic.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/OpaqueEquations.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/TransparentEquations.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/WellFoundedInstances.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Init.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/EqDecInstances.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Signature.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/EqDecInstances.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/CoreTactics.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Loader.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/FunctionalExtensionality.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Logic.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Tactics.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/NoConfusion.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Equations.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/NoConfusion.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Loader.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/All.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Signature.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/OpaqueEquations.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/NoConfusion.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/TransparentEquations.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/NoConfusion.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Loader.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Loader.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/FunctionalExtensionality.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/OpaqueEquations.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/Constants.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/TransparentEquations.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Prop/Constants.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Type/All.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Equations/Equations.glob
opam remove -y coq-equations.1.2.2+8.11