# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-num base Num library distributed with the OCaml compiler base-threads base base-unix base camlp5 7.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-perl 2 Virtual package relying on perl coq 8.5.0 Formal proof management system num 0 The Num library for arbitrary-precision integer and rational arithmetic ocaml 4.03.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.03.0 Official 4.03.0 release ocaml-config 1 OCaml Switch Configuration # opam file: opam-version: "2.0" maintainer: "gmalecha@gmail.com" homepage: "https://github.com/coq-community/coq-ext-lib" dev-repo: "git+https://github.com/coq-community/coq-ext-lib.git#8.5" bug-reports: "https://github.com/coq-community/coq-ext-lib/issues" authors: ["Gregory Malecha"] license: "BSD-2-Clause-FreeBSD" build: [ [make "-j%{jobs}%"] ] install: [ [make "install"] ] depends: [ "ocaml" "coq" {>= "8.5.0" & < "8.6~"} ] synopsis: "A library of Coq definitions, theorems, and tactics" url { src: "https://github.com/coq-community/coq-ext-lib/archive/v0.9.3.tar.gz" checksum: "md5=5c9c13afd1c7629377715091b3e17d23" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-ext-lib.0.9.3 coq.8.5.0
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 4h opam install -y --deps-only coq-ext-lib.0.9.3 coq.8.5.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-ext-lib.0.9.3 coq.8.5.0
Total: 2 M
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/HList.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/List.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Map/FMapPositive.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Generic/Ind.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Set/TwoThreeTrees.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Programming/Show.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/String.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Option.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Pair.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/SumN.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Nat.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Generic/DerivingData.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/Sets.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Vector.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/ListFirstnSkipn.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Member.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/PList.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Graph/GraphAdjList.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Programming/Extras.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Generic/Data.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Set/ListSet.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Graph/GraphAlgos.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/SigT.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Fin.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Map/FMapAList.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Generic/Func.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Z.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/StateMonad.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Map/FMapTwoThreeK.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Char.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Tuple.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/EitherMonad.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Relations/TransitiveClosure.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Core/Type.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/WriterMonad.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Tactics/Parametric.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Programming/Injection.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Sum.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Tactics/EqDep.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Programming/Le.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Programming/With.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/OptionMonad.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/ListNth.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/FuelMonad.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/ReaderMonad.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/Maps.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/EqDep.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Positive.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/OptionMonadLaws.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Tactics/Consider.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Tactics/Reify.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/Monad.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/Foldable.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Core/EquivDec.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/FunctorLaws.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Tactics.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Core/RelDec.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/FuelMonadLaws.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/N.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/ListMonad.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Graph/BuildGraph.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Prop.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Core/CmpDec.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Programming/Eqv.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Recur/Measure.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/PreFun.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/MonadFix.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Eq.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/PPair.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Fun.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/Monoid.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/Reducible.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/MonadWriter.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/Proper.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/Applicative.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Tactics/Cases.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Eq/UIP_trans.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/Functor.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Tactics/BoolTac.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Recur/Relation.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/MonadState.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/CoFunctor.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Tactics/TypeTac.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/Identity.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/POption.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Unit.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/BinOps.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Checked.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/MonadReader.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Recur/GenRec.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/ReaderMonadLaws.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/IdentityMonadLaws.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Tactics/MonadTac.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/MonadPlus.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/MonadLaws.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Bool.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/Traversable.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/IdentityMonad.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Lazy.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/LazyList.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/Monads.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Tactics/Injection.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/MonadExc.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/MonadZero.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Graph/Graph.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Set/SetMap.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/CoMonad.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/MonadCont.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Structures/MonadTrans.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Recur/Facts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Core/Any.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/ExtLib.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Tactics/Forward.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Tactics/Equality.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Stream.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Relations/Compose.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ExtLib/Data/Monads/ContMonad.vo
opam remove -y coq-ext-lib.0.9.3