# 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.14.0 Formal proof management system
dune 3.6.2 Fast, portable, and opinionated build system
ocaml 4.12.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.12.1 Official release 4.12.1
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.5 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
authors: [
"Massachusetts Institute of Technology"
]
maintainer: "Jason Gross <jgross@mit.edu>"
homepage: "https://github.com/mit-plv/coqutil"
bug-reports: "https://github.com/mit-plv/coqutil/issues"
license: "MIT"
build: [
[make "-j%{jobs}%"]
]
install: [make "install"]
depends: [
"conf-findutils" {build}
"coq" {>= "8.11~"}
]
conflict-class: [
"coq-coqutil"
]
dev-repo: "git+https://github.com/mit-plv/coqutil.git"
synopsis: "Coq library for tactics, basic definitions, sets, maps"
description: """
### coqutil -- Various Coq Utilities
Contents:
* [Datatypes](https://github.com/mit-plv/coqutil/tree/master/src/coqutil/Datatypes): Some utilities for existing datatypes, and new datatypes.
* [Decidable](https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Decidable.v): `BoolSpec`-based decidability typeclasses. Allows one to write `if MyType_eqb a b then ... else ...` where `MyType_eqb a b` returns a `bool`, instead of writing `if MyType_eq_dec a b then ... else ...` where `MyType_eq_dec a b` returns a `sumbool`, while still getting `a = b` and `a <> b` as hypotheses (as opposed to `MyType_eqb a b = true` and `MyType_eqb a b = false`) after destructing the `if` (need to use [`destr`](https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Tactics/destr.v) instead of `destruct`). So one gets the benefits of `Sumbool` without getting its disadvantage of having to carry around proof terms, which can cause a blow-up under reduction if one is not careful.
* [Map](https://github.com/mit-plv/coqutil/tree/master/src/coqutil/Map): A typeclass based map library allowing one to abstract over the concrete implementation of maps. The implementations have to be extensional, which excludes certain efficient implementations, but simplifies proofs, because one can `replace mapA with mapB` if one can prove that `mapA` and `mapB` have the same contents. Comes with a [solver](https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Map/Solver.v) which works reasonably fast on most map goals we have encountered so far.
* [Tactics](https://github.com/mit-plv/coqutil/tree/master/src/coqutil/Tactics): A collection of useful general-purpose tactics.
* [Word](https://github.com/mit-plv/coqutil/tree/master/src/coqutil/Word): Fixed width words for any width, in the same typeclass based style as the map library. Designed for the case where all words have the same (potentially abstract) bit width. Therefore, it does not provide functions to concatenate and split words, which is better addressed by [bbv](https://github.com/mit-plv/bbv/).
* [Z](https://github.com/mit-plv/coqutil/tree/master/src/coqutil/Z): Utilities to work with the `Z` type from Coq's standard library, including a tactic to prove `Z` equalities by splitting the equality into equalities on bit index ranges, a tactic to make `lia` capable of reasoning about goals with division and modulo, and a tactic to simplify expressions containing nested occurrences of `mod`, and more misc utilities.
* Various macros, notations, and desirable default settings.
Each feature is intended to be as minimal and as independent of the other features as possible, so that users can pick just what they need.
"""
tags: ["logpath:coqutil"]
url {
src: "https://github.com/mit-plv/coqutil/archive/refs/tags/v0.0.2.tar.gz"
checksum: "sha512=f3d37d57fb4301cbf6ab0bdd65c78bf5906607775b483e4f1b29e02e2a09980ef97ed7a9f19629d41bec45e281d7212cbb150e2602a26d30f408dd012ba51230"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-coqutil.0.0.2 coq.8.14.0Dry 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-coqutil.0.0.2 coq.8.14.0opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-coqutil.0.0.2 coq.8.14.0Total: 6 M
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/List.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Properties.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/List.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Properties.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Properties.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Properties.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Solver.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/TestGoals.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/OperatorOverloading.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/OperatorOverloading.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SortedList.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Properties.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/PropSet.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/OfListWord.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/MapEauto.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/List.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/ListSet.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/LittleEndianList.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Naive.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Interface.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Interface.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/BitOps.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/TestGoals.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/ZLib.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/OfFunc.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/prove_Zeq_bitwise.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/ZList.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/LittleEndian.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/PropSet.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/BigEndian.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/bitblast.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/SimplWordExpr.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SlowGoals.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SortedList.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/OfListWord.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/BitOps.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SlowGoals.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Sorting/OrderToPermutation.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Solver.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/ListSet.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_core.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/ZLib.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/Tactics.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/ZifyLittleEndian.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Interface.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/div_mod_to_equations.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/MapEauto.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/HList.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Funext.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/String.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SortedListWord.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/MapKeys.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/Simp.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/PushPullMod.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Byte.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Naive.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/Option.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/SafeSimpl.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/Prod.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Decidable.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/DebugWordEq.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/ToConversion.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/Inhabited.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/LittleEndianList.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Z_keyed_SortedListMap.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_map_hints.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Interface.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/rewr.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/forward.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Empty_set_keyed_map.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/prove_Zeq_bitwise.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_list_hints.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Properties.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/Lia.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/ZList.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/OfOptionListZ.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SortedListString.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Macros/ident_to_string.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/OperatorOverloading.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Solver.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/OfFunc.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_word_hints.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SortedListString_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/HList.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Bitwidth.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/ident_of_string.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Bitwidth64.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Bitwidth32.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/Records.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/bitblast.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Sorting/OrderToPermutation.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/destr.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_arith_hints.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/div_mod_to_equations.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/LittleEndian.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/div_to_equations.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SortedList.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Byte.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/ZifyLittleEndian.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/syntactic_unify.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/PropSet.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/TestGoals.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/SimplWordExpr.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/ToConversion.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/ListSet.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Funext.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/MapKeys.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/Option.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Sorting/Permutation.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/eplace.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/ltac_list_ops.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/OfListWord.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/String.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/BigEndian.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/simpl_rewrite.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SortedListWord.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Naive.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Decidable.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/ParamRecords.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/ZLib.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/Prod.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/prove_Zeq_bitwise.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/BitOps.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/rewr.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SortedListString_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/MapEauto.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_core.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/ZList.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/LittleEndianList.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Interface.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SlowGoals.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Macros/symmetry.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_core.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/PrimitivePair.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/bitblast.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/OfFunc.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/autoforward.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/Simp.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/SimplWordExpr.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/LittleEndian.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/forward.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/Records.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/ltac_list_ops.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/HList.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/PushPullMod.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Macros/symmetry.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/eabstract.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Sorting/OrderToPermutation.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/SafeSimpl.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Constr.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/ToConversion.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/div_mod_to_equations.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Decidable.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/rdelta.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/Records.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/eplace.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Interface.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/Tactics.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/letexists.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/rewr.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Byte.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Log.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Macros/ident_to_string.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/eplace.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Msg.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_map_hints.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/syntactic_unify.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/Inhabited.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/DebugWordEq.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/ZifyLittleEndian.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/BigEndian.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/ParamRecords.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Z_keyed_SortedListMap.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/dlet.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/String.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/sanity.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/simpl_rewrite.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/ident_of_string.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/Tactics.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Macros/unique.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/Simp.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/Option.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/Lia.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/Lia.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Macros/subst.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/Prod.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Funext.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/MapKeys.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/OfOptionListZ.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_map_hints.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/ident_of_string.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/forward.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/PushPullMod.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/ltac_list_ops.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Macros/ident_to_string.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/PrimitivePair.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Empty_set_keyed_map.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SortedListString.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/syntactic_unify.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/autoforward.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/DebugWordEq.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_list_hints.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Constr.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Macros/symmetry.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SortedListWord.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/Inhabited.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_arith_hints.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/destr.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SortedListString_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/letexists.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Datatypes/PrimitivePair.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_word_hints.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_arith_hints.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/sanity.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Z_keyed_SortedListMap.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/eabstract.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_list_hints.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/autoforward.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/SortedListString.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/div_to_equations.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/OfOptionListZ.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Z/div_to_equations.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/SafeSimpl.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/rdelta.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/destr.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/letexists.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd_word_hints.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/dlet.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Map/Empty_set_keyed_map.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Bitwidth.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Bitwidth64.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Bitwidth32.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Log.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/simpl_rewrite.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/dlet.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/fwd.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Macros/unique.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Sorting/Permutation.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/ParamRecords.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Bitwidth.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Bitwidth64.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Word/Bitwidth32.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Constr.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Msg.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Sorting/Permutation.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Macros/subst.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Macros/subst.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Log.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Msg.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Macros/unique.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/eabstract.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/Tactics/rdelta.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/coqutil/sanity.globopam remove -y coq-coqutil.0.0.2