# 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.17.1 The Coq Proof Assistant
coq-core 8.17.1 The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib 8.17.1 The Coq Proof Assistant -- Standard Library
coqide-server 8.17.1 The Coq Proof Assistant, XML protocol server
dune 3.12.2 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"
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.15~"}
]
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.4.tar.gz"
checksum: "sha512=d8edb84e9a68de786368b27212f500f8f472ffc72fd715facb89b66ad75b69319e40b42eb53a8e68212379aa5e21c0c5b827411ec1790f956d65762372f7d6be"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-coqutil.0.0.4 coq.8.17.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-coqutil.0.0.4 coq.8.17.1opam list; echo; timeout 4h opam install -y -v coq-coqutil.0.0.4 coq.8.17.1Total: 7 M
../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/List.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Properties.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/List.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Properties.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Properties.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Properties.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Solver.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/OperatorOverloading.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/OperatorOverloading.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/SortedList.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Properties.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/PropSet.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/OfListWord.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/ZList.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/MapEauto.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/List.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/ListSet.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/LittleEndianList.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Naive.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Interface.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Interface.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/BitOps.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/ZLib.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/OfFunc.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/prove_Zeq_bitwise.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/RecordSetters.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/LittleEndian.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/PropSet.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/BigEndian.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/Result.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/RecordSettersUsingExistingGetters.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/bitblast.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/SortedList.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/RecordSetters.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/RecordSettersUsingExistingGetters.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/ZList.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/OfListWord.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/BitOps.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/SimplWordExpr.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ident_to_string.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Sorting/OrderToPermutation.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Solver.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/ListSet.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_core.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/ZLib.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/Tactics.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Interface.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/div_mod_to_equations.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/MapEauto.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/String.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/HList.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Funext.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/ZifyLittleEndian.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/SortedListWord.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/Simp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/MapKeys.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/PushPullMod.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Byte.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Naive.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/SafeSimpl.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Properties.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/RecordSetters.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/Option.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Decidable.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/Lia.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/DebugWordEq.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/Inhabited.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/ToConversion.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/LittleEndianList.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/Prod.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ident_to_string.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Z_keyed_SortedListMap.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Interface.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_map_hints.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/rewr.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/forward.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Empty_set_keyed_map.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/prove_Zeq_bitwise.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/OfOptionListZ.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_list_hints.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/SortedListString.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/RecordSettersUsingExistingGetters.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/OperatorOverloading.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Solver.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/OfFunc.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_word_hints.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Lia.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/Result.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/HList.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Bitwidth.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/WithQualName.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/WithBaseName.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Bitwidth64.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Bitwidth32.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/Records.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ident_of_string.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/bitblast.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Sorting/OrderToPermutation.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/reference_to_string.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/destr.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/ident_to_string.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_arith_hints.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Ring.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/pattern_tuple.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/div_mod_to_equations.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/LittleEndian.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/div_to_equations.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/SortedList.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/foreach_hyp.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Byte.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/ZifyLittleEndian.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/PropSet.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/syntactic_unify.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ltac_list_ops.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/ToConversion.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/ListSet.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Funext.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/MapKeys.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/Option.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Sorting/Permutation.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/ZList.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/OfListWord.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/eplace.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/String.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/SimplWordExpr.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/pattern_tuple.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/BigEndian.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Notations.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/SortedListWord.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/simpl_rewrite.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ParamRecords.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Naive.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Decidable.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/ZLib.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/Prod.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/prove_Zeq_bitwise.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/BitOps.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/rewr.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/RecordEta.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/foreach_hyp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_core.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/MapEauto.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fold_hyps.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/Lia.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ident_ops.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_core.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fold_hyps.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/LittleEndianList.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Interface.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/symmetry.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ltac_list_ops.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/PrimitivePair.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/bitblast.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/OfFunc.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Std.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/Simp.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Failf.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/String.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/Result.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fold_hyps.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/autoforward.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/List.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/forward.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/rdelta.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/Records.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/LittleEndian.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/evar_free.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/SimplWordExpr.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/HList.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/PushPullMod.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Constr.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Ltac2.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Ident.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Sorting/OrderToPermutation.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/grepeat.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/SafeSimpl.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/WithQualName.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/symmetry.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/WithBaseName.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/eabstract.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/ToConversion.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Control.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/div_mod_to_equations.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Decidable.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/let_binding_to_eq.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/Records.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/eplace.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Pervasives.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Interface.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/rdelta.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ident_ops.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/Tactics.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/foreach_hyp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Char.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/letexists.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/rewr.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Byte.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/dlist.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/eplace.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/Lia.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/pattern_tuple.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_map_hints.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/syntactic_unify.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ident_to_string.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/Inhabited.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/DebugWordEq.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/ZifyLittleEndian.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/BigEndian.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ident_ops.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/ident_to_string.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Z_keyed_SortedListMap.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ParamRecords.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/String.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/simpl_rewrite.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/Tactics.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/Simp.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/Option.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/dlet.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/sanity.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/unique.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ident_of_string.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/Prod.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Notations.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/RecordEta.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ltac_list_ops.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/subst.vo../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Funext.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/MapKeys.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/grepeat.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/OfOptionListZ.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_map_hints.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/String.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/forward.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/PushPullMod.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Empty_set_keyed_map.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/PrimitivePair.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/SortedListString.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/reference_to_string.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Std.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Notations.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/List.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/syntactic_unify.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/autoforward.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/WithQualName.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/WithBaseName.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Failf.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/rdelta.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/DebugWordEq.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_list_hints.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Constr.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/symmetry.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/SortedListWord.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/Inhabited.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_arith_hints.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/destr.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/grepeat.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/letexists.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/evar_free.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ident_of_string.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/PrimitivePair.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_word_hints.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_arith_hints.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/ident_to_string.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/sanity.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Z_keyed_SortedListMap.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/evar_free.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/eabstract.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_list_hints.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/autoforward.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/SortedListString.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/div_to_equations.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/letexists.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/OfOptionListZ.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Z/div_to_equations.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/SafeSimpl.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/rdelta.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/destr.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/let_binding_to_eq.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd_word_hints.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/dlet.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Map/Empty_set_keyed_map.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Ident.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Ltac2.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Ltac2.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/reference_to_string.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Bitwidth.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Failf.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Pervasives.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/let_binding_to_eq.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Control.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Bitwidth64.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Bitwidth32.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/simpl_rewrite.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Lia.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/dlist.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/dlet.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/fwd.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/unique.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Std.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Sorting/Permutation.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Lia.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/rdelta.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/RecordEta.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Bitwidth.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Bitwidth64.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Word/Bitwidth32.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/List.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Ident.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Control.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/String.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Ring.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Ring.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/ParamRecords.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Constr.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Sorting/Permutation.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Char.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/subst.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Pervasives.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/subst.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Ltac2Lib/Char.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Macros/unique.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Datatypes/dlist.v../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/eabstract.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/Tactics/rdelta.glob../ocaml-base-compiler.5.0.0/lib/coq/user-contrib/coqutil/sanity.globopam remove -y coq-coqutil.0.0.4