« Up

rewriter 0.0.2 29 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.13.0      Formal proof management system
num                 1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.11.2      The OCaml compiler (virtual package)
ocaml-base-compiler 4.11.2      Official release 4.11.2
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.3       A library manager for OCaml
zarith              1.12        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
authors: [
  "Google Inc."
  "Massachusetts Institute of Technology"
]
maintainer: "Jason Gross <jgross@mit.edu>"
homepage: "https://github.com/mit-plv/rewriter"
bug-reports: "https://github.com/mit-plv/rewriter/issues"
license: "MIT OR Apache-2.0 OR BSD-1-Clause"
build: [
  [make "-j%{jobs}%"]
]
install: [make "install"]
depends: [
  "ocaml"
  "coq" {>= "8.9~"}
]
dev-repo: "git+https://github.com/mit-plv/rewriter.git"
synopsis: "Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography"
tags: ["logpath:Rewriter"]
url {
  src: "https://github.com/mit-plv/rewriter/archive/refs/tags/v0.0.2.tar.gz"
  checksum: "sha512=3e555976dd2e2074253b0c1cfa473b436ddc08ca96125a42eff989c592814688775d17ef8a7ba0df32cea432f4f84287ef06425b273069faf58ce666e1009ce7"
}

Lint

Command

true

Return code

0

Dry install 🏜️

Dry install with the current Coq version:

Command

opam install -y --show-action coq-rewriter.0.0.2 coq.8.13.0

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-rewriter.0.0.2 coq.8.13.0

Return code

0

Duration

1 m 0 s

Install 🚀

Command

opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-rewriter.0.0.2 coq.8.13.0

Return code

0

Duration

29 m 0 s

Installation size

Total: 44 M

• 5 M ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo
• 4 M ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo
• 3 M ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo
• 3 M ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples.vo
• 3 M ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/ProofsCommon.vo
• 2 M ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/InterpProofs.vo
• 2 M ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PrefixSums.vo
• 2 M ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo
• 1 M ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/Wf.vo
• 1 M ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/UnderLetsProofs.vo
• 1 M ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Demo.vo
• 1020 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/Inversion.vo
• 953 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/ProofsCommon.glob
• 922 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Wf.vo
• 761 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/InterpProofs.glob
• 734 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/ListUtil.vo
• 638 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersLibrary.vo
• 618 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/Language.vo
• 538 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/Wf.glob
• 538 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/UnderLetsProofs.glob
• 498 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/ListUtil.glob
• 479 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Wf.glob
• 384 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Reify.vo
• 362 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Rewriter.vo
• 330 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/Language.glob
• 287 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Rewriter.glob
• 281 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersBasicLibrary.vo
• 255 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersLibraryProofs.vo
• 241 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/Inversion.glob
• 240 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/ListUtil/Forall.vo
• 228 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Sample.glob
• 226 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersLibrary.glob
• 225 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/ProofsCommon.v
• 217 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersBasicGenerate.vo
• 202 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.glob
• 201 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Sample.vo
• 178 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.glob
• 166 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Bool/Reflect.vo
• 162 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/NatUtil.vo
• 149 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/rewriter_build_plugin.cmxs
• 132 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersGenerate.vo
• 130 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/ListUtil/Forall.glob
• 128 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.glob
• 128 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Harness.vo
• 126 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Reify.glob
• 125 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/MSetPositive/Facts.vo
• 115 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/ProofsCommonTactics.vo
• 111 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Decidable.vo
• 111 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/ListUtil.v
• 110 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersLibraryProofs.glob
• 106 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/UnderLetsProofs.v
• 104 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/Wf.v
• 101 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/Language.v
• 99 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/InterpProofs.v
• 98 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/AllTactics.vo
• 97 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Bool/Reflect.glob
• 93 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Sum.vo
• 87 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersBasicGenerate.v
• 87 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Option.vo
• 81 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.glob
• 80 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Rewriter.v
• 79 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/NatUtil.glob
• 74 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Reify.v
• 73 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersBasicLibrary.glob
• 70 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Sigma.glob
• 69 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Harness.glob
• 69 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Wf.v
• 65 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/Inversion.v
• 64 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Option.glob
• 63 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Prod.vo
• 63 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/UnderLets.vo
• 63 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersBasicGenerate.glob
• 60 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Sigma.vo
• 58 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/ParseArithmetic.glob
• 58 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/ParseArithmetic.vo
• 56 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersGenerate.v
• 54 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersLibrary.v
• 51 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/FMapPositive/Equality.vo
• 49 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/ProofsCommonTactics.glob
• 48 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersGenerateProofs.vo
• 47 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/String.vo
• 47 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/Parse/Common.vo
• 45 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/inductive_from_elim_plugin.cmxs
• 44 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/PrimitiveProd.vo
• 43 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Sample.v
• 43 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/PrimitiveSigma.vo
• 41 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Prod.glob
• 41 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/PreLemmas.vo
• 41 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersGenerate.glob
• 41 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/ListUtil/SetoidList.vo
• 41 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/UnderLets.glob
• 40 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Equality.vo
• 39 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/String.glob
• 39 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Sum.glob
• 38 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/PrimitiveSigma.glob
• 38 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/definition_by_tactic_plugin.cmxs
• 37 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Decidable.glob
• 37 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Bool.vo
• 36 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Equality.glob
• 35 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/Parse/Common.glob
• 33 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/ProofsCommonTactics.v
• 33 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/AllTactics.glob
• 32 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/strategy_tactic_plugin.cmxs
• 31 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuildRegistry.vo
• 30 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/PrimitiveProd.glob
• 30 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuild.vo
• 30 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Settings.vo
• 30 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/OptionList.vo
• 30 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuildRegistryImports.vo
• 28 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Notations.vo
• 27 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersLibraryProofs.v
• 27 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Bool/Reflect.v
• 27 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/MSetPositive/Equality.vo
• 24 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/Decimal.vo
• 23 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/AllTactics.v
• 22 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v
• 21 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Bool.glob
• 21 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/rewriter_build_plugin.cmxa
• 21 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/Pre.vo
• 20 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/NatUtil.v
• 19 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Sigma/Related.vo
• 19 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/Ascii.vo
• 19 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.vo
• 19 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v
• 19 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/RewriteHyp.vo
• 18 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/PreLemmas.glob
• 18 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Pointed.vo
• 17 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PrefixSums.glob
• 16 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/ListUtil/SetoidList.glob
• 16 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Option.v
• 16 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Sigma/Related.glob
• 16 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/HProp.vo
• 15 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/ListUtil/Forall.v
• 15 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/OptionList.glob
• 15 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/LetIn.vo
• 15 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Sigma.v
• 14 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/BreakMatch.vo
• 14 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Harness.v
• 14 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/PrimitiveHList.vo
• 13 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v
• 13 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Comparison.vo
• 12 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Notations.v
• 12 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/String.v
• 12 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/PreCommon.vo
• 12 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/DebugPrint.vo
• 12 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/DestructHead.vo
• 12 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/definition_by_tactic_plugin.cmxa
• 11 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/ParseArithmetic.v
• 11 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Pointed.glob
• 11 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/UnderLets.v
• 11 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Logic/ExistsEqAnd.vo
• 11 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Decidable.v
• 11 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Prod.v
• 11 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/FixCoqMistakes.vo
• 11 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples.glob
• 10 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v
• 10 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/rewriter_build.cmx
• 10 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersGenerateProofs.glob
• 9 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/LetIn.glob
• 9 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/PrimitiveSigma.v
• 9 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Sum.v
• 9 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersGenerateProofs.v
• 9 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/strategy_tactic_plugin.cmxa
• 9 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Logic/ExistsEqAnd.glob
• 9 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Bool/Equality.vo
• 9 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/inductive_from_elim_plugin.cmxa
• 9 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/CacheTerm.vo
• 8 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Equality.v
• 8 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/PrimitiveProd.v
• 7 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Bool.v
• 7 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/RewriteHyp.v
• 7 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/CPSNotations.vo
• 7 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/InductiveHList.vo
• 7 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/Parse/Common.v
• 7 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/IffT.vo
• 7 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/IdentifiersBasicLibrary.v
• 7 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SplitInContext.vo
• 7 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/CPSId.vo
• 6 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/definition_by_tactic.cmi
• 6 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.glob
• 6 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/definition_by_tactic_plugin.cmx
• 6 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/definition_by_tactic.cmx
• 6 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/Pre.glob
• 6 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/strategy_tactic_plugin.cmx
• 6 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/definition_by_tactic_plugin.cmi
• 6 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/strategy_tactic_plugin.cmi
• 6 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/DestructHyps.vo
• 6 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/TypeList.vo
• 5 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SetoidSubst.vo
• 5 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/HProp.glob
• 5 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/Decimal.glob
• 5 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/ListUtil/SetoidList.v
• 5 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Isomorphism.vo
• 5 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/BreakMatch.v
• 5 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SpecializeBy.vo
• 5 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/CPSNotations.glob
• 5 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/inductive_from_elim_plugin.cmx
• 5 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/HeadUnderBinders.vo
• 5 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/rewriter_build_plugin.cmx
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/inductive_from_elim_plugin.cmi
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/DestructHead.v
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/rewriter_build_plugin.cmi
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/inductive_from_elim.cmx
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/PrimitiveHList.glob
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/UniquePose.vo
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Logic/ProdForall.vo
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/MSetPositive/Facts.glob
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/FindHyp.vo
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/DoWithHyp.vo
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/rewriter_build.cmi
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/FixCoqMistakes.v
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/RunTacticAsConstr.vo
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/Pre.v
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/FixCoqMistakes.glob
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/DebugPrint.glob
• 4 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/strategy_tactic.cmx
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/PreLemmas.v
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/inductive_from_elim.cmi
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/FMapPositive/Equality.glob
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SpecializeAllWays.vo
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/TransparentAssert.vo
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PrefixSums.v
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/Head.vo
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/AssertSucceedsPreserveError.vo
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/strategy_tactic.cmi
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/LetIn.v
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Pointed.v
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Sigma/Related.v
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/OptionList.v
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/HProp.v
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Demo.v
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/CacheTerm.v
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/Ascii.glob
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/PrintContext.vo
• 3 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/DebugPrint.v
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Demo.glob
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/InductiveHList.glob
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/WarnIfGoalsRemain.vo
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples.v
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/PrintGoal.vo
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/ConstrFail.vo
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/CPSNotations.v
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/EvarNormalize.vo
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/Contains.vo
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SubstEvars.vo
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/Not.vo
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/CPSId.v
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SetEvars.vo
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/StrategyTactic.vo
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/Test.vo
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/GetGoal.vo
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/GlobalSettings.vo
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/DestructHyps.v
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Logic/ProdForall.glob
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/PreCommon.glob
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SplitInContext.glob
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/Decimal.v
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SplitInContext.v
• 2 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Logic/ExistsEqAnd.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/MSetPositive/Facts.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/CPSId.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Isomorphism.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuildRegistry.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/TypeList.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SpecializeBy.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Isomorphism.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/MSetPositive/Equality.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/UniquePose.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/DestructHead.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Language/PreCommon.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/IffT.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/BreakMatch.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/FMapPositive/Equality.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/FindHyp.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SetoidSubst.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/GlobalSettings.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Strings/Ascii.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/StrategyTactic.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/HeadUnderBinders.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/InductiveHList.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/TransparentAssert.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/PrimitiveHList.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/RunTacticAsConstr.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/CacheTerm.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/DoWithHyp.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/TypeList.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuild.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/MSetPositive/Equality.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/IffT.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/ConstrFail.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuildRegistryImports.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/HeadUnderBinders.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/PrintContext.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuildRegistryImports.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Settings.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SpecializeBy.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Settings.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/RunTacticAsConstr.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/Contains.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SpecializeAllWays.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/AssertSucceedsPreserveError.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/Not.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/WarnIfGoalsRemain.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/Head.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/PrintGoal.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/Test.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SpecializeAllWays.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/PrintContext.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/EvarNormalize.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Notations.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/DoWithHyp.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Logic/ProdForall.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/RewriteHyp.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/UniquePose.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuildRegistry.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Bool/Equality.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuild.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/AssertSucceedsPreserveError.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SetEvars.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/WarnIfGoalsRemain.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/PrintGoal.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SetoidSubst.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/DestructHyps.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/FindHyp.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/Head.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/Not.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Comparison.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SubstEvars.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/TransparentAssert.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/EvarNormalize.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/plugins/StrategyTactic.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SubstEvars.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/ConstrFail.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/SetEvars.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/Contains.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/GetGoal.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/GlobalSettings.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/Test.glob
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Bool/Equality.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Tactics/GetGoal.v
• 1 K ../ocaml-base-compiler.4.11.2/lib/coq/user-contrib/Rewriter/Util/Comparison.v

Uninstall 🧹

Command

opam remove -y coq-rewriter.0.0.2

Return code

0

Missing removes

none

Wrong removes

none