« Up

coqutil 0.0.2 4 m 0 s 🏆

Context

# 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.15.2      Formal proof management system
dune                  3.6.2       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.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"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-coqutil.0.0.2 coq.8.15.2
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-coqutil.0.0.2 coq.8.15.2
Return code
0
Duration
1 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-coqutil.0.0.2 coq.8.15.2
Return code
0
Duration
4 m 0 s

Installation size

Total: 6 M

  • 547 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/List.vo
  • 422 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Properties.vo
  • 377 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/List.glob
  • 355 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Properties.glob
  • 208 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Properties.vo
  • 187 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Properties.glob
  • 119 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Solver.vo
  • 110 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/TestGoals.vo
  • 105 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/OperatorOverloading.vo
  • 102 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/OperatorOverloading.glob
  • 94 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SortedList.vo
  • 86 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Properties.v
  • 80 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/PropSet.vo
  • 79 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/OfListWord.vo
  • 74 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/MapEauto.vo
  • 69 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/List.v
  • 67 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/ListSet.vo
  • 66 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Naive.vo
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/LittleEndianList.vo
  • 64 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Interface.vo
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Interface.vo
  • 60 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/BitOps.vo
  • 60 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/TestGoals.glob
  • 58 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/ZLib.vo
  • 56 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/OfFunc.vo
  • 56 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/prove_Zeq_bitwise.vo
  • 55 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/ZList.vo
  • 53 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/LittleEndian.vo
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/PropSet.glob
  • 50 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/BigEndian.vo
  • 49 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/bitblast.vo
  • 45 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/SimplWordExpr.vo
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SlowGoals.glob
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SortedList.glob
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/OfListWord.glob
  • 42 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/BitOps.glob
  • 42 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SlowGoals.vo
  • 39 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Sorting/OrderToPermutation.vo
  • 39 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Solver.glob
  • 36 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/ListSet.glob
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_core.vo
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/ZLib.glob
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/Tactics.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Interface.glob
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/ZifyLittleEndian.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/div_mod_to_equations.vo
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/MapEauto.glob
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/HList.vo
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Funext.vo
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/String.vo
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SortedListWord.vo
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/MapKeys.vo
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/Simp.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/PushPullMod.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Byte.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Naive.glob
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/SafeSimpl.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/Option.vo
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Decidable.vo
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/Prod.vo
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/DebugWordEq.vo
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/Inhabited.vo
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/LittleEndianList.glob
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/ToConversion.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Z_keyed_SortedListMap.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_map_hints.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Interface.glob
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/forward.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/rewr.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Empty_set_keyed_map.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/prove_Zeq_bitwise.glob
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Properties.v
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_list_hints.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/Lia.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/ZList.glob
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/OfOptionListZ.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SortedListString.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/OperatorOverloading.v
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Macros/ident_to_string.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Solver.v
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/OfFunc.glob
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_word_hints.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SortedListString_test.vo
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/HList.glob
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Bitwidth.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/ident_of_string.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Bitwidth64.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Bitwidth32.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/bitblast.glob
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/Records.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Sorting/OrderToPermutation.glob
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/destr.vo
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_arith_hints.vo
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/div_mod_to_equations.glob
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/LittleEndian.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/div_to_equations.vo
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SortedList.v
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Byte.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/ZifyLittleEndian.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/syntactic_unify.vo
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/PropSet.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/TestGoals.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/SimplWordExpr.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/ToConversion.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Funext.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/ListSet.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/MapKeys.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/Option.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Sorting/Permutation.vo
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/eplace.vo
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/OfListWord.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/ltac_list_ops.vo
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/String.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/BigEndian.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SortedListWord.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/simpl_rewrite.vo
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Naive.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Decidable.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/ParamRecords.vo
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/ZLib.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/Prod.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/prove_Zeq_bitwise.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/BitOps.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/rewr.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SortedListString_test.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/MapEauto.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_core.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/ZList.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/LittleEndianList.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/PrimitivePair.vo
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Interface.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SlowGoals.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Macros/symmetry.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_core.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/bitblast.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/OfFunc.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/autoforward.vo
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/Simp.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/SimplWordExpr.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/LittleEndian.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/forward.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/Records.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/ltac_list_ops.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/HList.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/PushPullMod.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Macros/symmetry.vo
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/eabstract.vo
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Sorting/OrderToPermutation.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/SafeSimpl.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Constr.vo
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/ToConversion.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/div_mod_to_equations.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Decidable.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/Records.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/rdelta.vo
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/eplace.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Interface.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/Tactics.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/letexists.vo
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/rewr.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Byte.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Log.vo
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Macros/ident_to_string.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/eplace.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Msg.vo
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_map_hints.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/syntactic_unify.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/Inhabited.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/DebugWordEq.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/ZifyLittleEndian.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/BigEndian.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/ParamRecords.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Z_keyed_SortedListMap.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/String.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/simpl_rewrite.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/ident_of_string.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/dlet.vo
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/sanity.vo
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/Tactics.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/Simp.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/Option.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Macros/unique.vo
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/Lia.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/Lia.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/Prod.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Macros/subst.vo
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Funext.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/MapKeys.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/OfOptionListZ.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/ident_of_string.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_map_hints.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Macros/ident_to_string.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/forward.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/PushPullMod.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/ltac_list_ops.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/PrimitivePair.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Empty_set_keyed_map.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SortedListString.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/syntactic_unify.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/autoforward.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/DebugWordEq.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_list_hints.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Constr.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Macros/symmetry.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SortedListWord.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/Inhabited.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_arith_hints.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/destr.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SortedListString_test.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/letexists.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Datatypes/PrimitivePair.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_word_hints.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_arith_hints.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/sanity.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Z_keyed_SortedListMap.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/eabstract.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_list_hints.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/autoforward.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/SortedListString.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/div_to_equations.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/OfOptionListZ.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Z/div_to_equations.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/SafeSimpl.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/rdelta.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/destr.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/letexists.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd_word_hints.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/dlet.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Map/Empty_set_keyed_map.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Bitwidth.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Bitwidth64.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Bitwidth32.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Log.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/simpl_rewrite.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/dlet.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/fwd.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Macros/unique.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Sorting/Permutation.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/ParamRecords.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Bitwidth.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Bitwidth64.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Word/Bitwidth32.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Constr.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Msg.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Sorting/Permutation.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Macros/subst.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Macros/subst.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Log.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Ltac2Lib/Msg.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Macros/unique.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/eabstract.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/Tactics/rdelta.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/coqutil/sanity.glob

Uninstall 🧹

Command
opam remove -y coq-coqutil.0.0.2
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣