# 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.13.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.13.1 Official release 4.13.1
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: "A library of Coq definitions, theorems, and tactics"
description:
"A collection of theories and plugins that may be useful in other Coq developments."
maintainer: "gmalecha@gmail.com"
authors: "Gregory Malecha"
license: "BSD-2-Clause"
tags: "logpath:ExtLib"
homepage: "https://github.com/coq-community/coq-ext-lib"
bug-reports: "https://github.com/coq-community/coq-ext-lib/issues"
depends: [
"ocaml"
"coq" {>= "8.9" & (< "8.10" | >= "8.11")}
]
build: [make "-j%{jobs}%" "theories"]
run-test: [make "-j%{jobs}%" "examples"]
install: [make "install"]
dev-repo: "git+https://github.com/coq-community/coq-ext-lib.git"
url {
src:
"https://github.com/coq-community/coq-ext-lib/archive/refs/tags/v0.12.0.tar.gz"
checksum: [
"md5=ab08c703d854fdb90f35cf40614e089a"
"sha512=8cf5853137f21bae34382b7e91278625cf18e7a484464832f69b634984b27d00adb290b0132a476547ebb657858ee80c3b67a9c699b8b19a5ae47a6b25b445d0"
]
}
trueDry install with the current Coq version:
opam install -y --show-action coq-ext-lib.0.12.0 coq.8.16.1Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-ext-lib.0.12.0 coq.8.16.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-ext-lib.0.12.0 coq.8.16.1Total: 3 M
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/HList.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/HList.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Map/FMapPositive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/List.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Generic/Ind.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Map/FMapAList.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Pair.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Set/TwoThreeTrees.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Show.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/SumN.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Vector.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Option.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/PList.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/String.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadLaws.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Sets.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Member.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Set/TwoThreeTrees.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Generic/DerivingData.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/ListFirstnSkipn.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/WriterMonad.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Generic/Data.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Nat.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/HList.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Map/FMapAList.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Fin.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Relations/TransitiveClosure.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Extras.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Map/FMapPositive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Map/FMapTwoThreeK.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Graph/GraphAdjList.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/StateMonad.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/List.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Generic/Func.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/WriterMonad.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Parametric.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Z.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Tuple.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Set/ListSet.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Le.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Graph/GraphAlgos.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Char.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Map/FMapTwoThreeK.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Maps.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Sum.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/EqDep.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/PList.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/Decision.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/StateMonad.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/EitherMonad.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Generic/Ind.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Vector.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Relations/TransitiveClosure.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/ListNth.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/With.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Set/TwoThreeTrees.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/ReaderMonad.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/OptionMonad.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Consider.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Show.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/SigT.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Eq.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Pair.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/String.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/FuelMonad.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/PPair.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Sets.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/EqDep.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Generic/Data.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/SumN.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Injection.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Extras.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadLaws.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Reify.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Consider.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Foldable.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/RelDec.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Parametric.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Generic/Func.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/CmpDec.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Prop.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/RelDec.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/OptionMonadLaws.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Le.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Positive.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Option.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadFix.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/EitherMonad.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/ReaderMonad.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/EquivDec.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Member.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Eqv.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadFix.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Monad.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/OptionMonadLaws.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Maps.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Eq/UIP_trans.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/OptionMonad.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Prop.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Graph/BuildGraph.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Recur/Measure.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Cases.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/FuelMonadLaws.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/PPair.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Sum.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Generic/DerivingData.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Monad.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Reducible.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/ListFirstnSkipn.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/POption.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/With.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Map/FMapPositive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/BoolTac.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Fin.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/N.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Eq.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Set/ListSet.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Fun.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/ListNth.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Eqv.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Reducible.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadWriter.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/CmpDec.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/CoMonadLaws.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/PList.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/FunctorLaws.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Eq/UIP_trans.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Recur/Relation.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Map/FMapAList.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/ContMonad.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/List.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Monoid.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Graph/GraphAdjList.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Tuple.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Recur/GenRec.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadState.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Vector.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Nat.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/CoFunctor.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Generic/Data.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Applicative.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Forward.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Map/FMapTwoThreeK.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Foldable.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Checked.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Fun.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/WriterMonad.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Recur/GenRec.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Graph/GraphAlgos.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/POption.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Show.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/IdentityMonadLaws.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/BinOps.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/ReaderMonadLaws.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadReader.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/MonadTac.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/String.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadPlus.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadWriter.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Option.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Bool.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/FuelMonad.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Generic/Ind.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Graph/BuildGraph.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/FuelMonadLaws.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Traversable.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Injection.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/CoMonad.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/SigT.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/SumN.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/IdentityMonad.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadState.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Lazy.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/ContMonad.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/LazyList.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/RelDec.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadReader.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Unit.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Consider.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Relations/TransitiveClosure.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadExc.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Le.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/EqDep.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/BoolTac.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/EqDep.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Char.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadZero.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Applicative.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Recur/Measure.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Member.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/BinOps.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Pair.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Functor.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/StateMonad.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/Decision.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Parametric.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Graph/Graph.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadCont.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadTrans.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Positive.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Monads.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Hide.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/PreFun.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/ExtLib.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Sum.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Traversable.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Fin.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Monad.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Recur/Facts.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/OptionMonad.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Set/SetMap.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/ReaderMonadLaws.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Eq.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/EitherMonad.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Checked.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Reify.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/Any.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/ReaderMonad.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Z.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Sets.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Generic/Func.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Cases.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Extras.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/PPair.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Maps.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Prop.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Eq/UIP_trans.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadLaws.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/CoFunctor.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/EqDep.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Equality.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Recur/Facts.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Generic/DerivingData.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/POption.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/ListNth.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Nat.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Lazy.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Relations/Compose.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Stream.vo../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/ListFirstnSkipn.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/CoMonadLaws.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadPlus.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Reducible.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Char.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/FunctorLaws.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/BoolTac.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/IdentityMonadLaws.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Set/ListSet.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Graph/GraphAdjList.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/ContMonad.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadFix.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Eqv.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/CmpDec.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/FuelMonad.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/With.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/CoMonad.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Forward.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Graph/GraphAlgos.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Tuple.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Monoid.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Injection.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Recur/Relation.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Fun.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Z.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Positive.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Graph/BuildGraph.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Functor.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Forward.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/LazyList.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/SigT.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/EquivDec.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadExc.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/EqDep.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Recur/GenRec.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadWriter.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Recur/Measure.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Checked.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadZero.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Foldable.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/IdentityMonad.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadState.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Relations/Compose.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/PreFun.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadCont.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Applicative.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadReader.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/MonadTac.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Graph/Graph.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Injection.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Recur/Relation.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Bool.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Injection.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Lazy.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/Decision.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Traversable.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/CoFunctor.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Set/SetMap.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Hide.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/BinOps.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Reify.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Stream.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Programming/Injection.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/CoMonadLaws.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadTrans.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Monads.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Monoid.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadPlus.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Bool.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Unit.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/CoMonad.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Monads.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/FunctorLaws.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Recur/Facts.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/Functor.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Hide.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/Any.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/Any.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/FuelMonadLaws.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/OptionMonadLaws.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Core/EquivDec.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/IdentityMonad.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/PreFun.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadZero.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/IdentityMonadLaws.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Monads/ReaderMonadLaws.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/LazyList.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Equality.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Cases.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Unit.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Graph/Graph.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadExc.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Stream.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadCont.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Structures/MonadTrans.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Relations/Compose.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/MonadTac.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/Set/SetMap.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Tactics/Equality.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/ExtLib.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/N.glob../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/ExtLib.v../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/ExtLib/Data/N.vopam remove -y coq-ext-lib.0.12.0