# 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.1 Formal proof management system
dune 3.4.1 Fast, portable, and opinionated build system
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
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: [
"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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-rewriter.0.0.2 coq.8.15.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-rewriter.0.0.2 coq.8.15.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-rewriter.0.0.2 coq.8.15.1Total: 41 M
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/ProofsCommon.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/InterpProofs.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/Wf.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/UnderLetsProofs.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PrefixSums.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/Inversion.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Wf.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/ProofsCommon.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/InterpProofs.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/ListUtil.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Demo.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersLibrary.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/Language.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/Wf.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/UnderLetsProofs.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/ListUtil.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Wf.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Reify.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Rewriter.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersBasicLibrary.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/Language.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Rewriter.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersLibraryProofs.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersBasicGenerate.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/ListUtil/Forall.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/Inversion.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Sample.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersLibrary.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/ProofsCommon.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Sample.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/rewriter_build_plugin.cmxs../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Bool/Reflect.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/NatUtil.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersGenerate.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Harness.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Reify.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/ListUtil/Forall.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/ProofsCommonTactics.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/MSetPositive/Facts.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Decidable.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/ListUtil.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersLibraryProofs.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/UnderLetsProofs.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/Wf.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/AllTactics.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/Language.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/InterpProofs.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Bool/Reflect.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Sum.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersBasicGenerate.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Option.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Rewriter.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/NatUtil.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Reify.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersBasicLibrary.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Sigma.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Harness.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Wf.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersBasicGenerate.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/Inversion.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Option.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Prod.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/UnderLets.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/ParseArithmetic.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Sigma.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/ParseArithmetic.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersGenerate.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersLibrary.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/ProofsCommonTactics.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersGenerateProofs.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/FMapPositive/Equality.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersGenerate.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/String.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/inductive_from_elim_plugin.cmxs../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/Parse/Common.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/PrimitiveProd.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Sample.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/PrimitiveSigma.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Prod.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/PreLemmas.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/ListUtil/SetoidList.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/definition_by_tactic_plugin.cmxs../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/UnderLets.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/String.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Sum.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/PrimitiveSigma.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Equality.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Bool.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Decidable.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/AllTactics.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Equality.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/Parse/Common.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/ProofsCommonTactics.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/strategy_tactic_plugin.cmxs../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuildRegistry.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/OptionList.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/PrimitiveProd.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuild.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Settings.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuildRegistryImports.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/MSetPositive/Equality.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Notations.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersLibraryProofs.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Bool/Reflect.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/Decimal.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/AllTactics.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/RewriteHyp.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Bool.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/Pre.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/NatUtil.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/rewriter_build_plugin.cmxa../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Sigma/Related.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/Ascii.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/PreLemmas.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Pointed.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PrefixSums.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/BreakMatch.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/ListUtil/SetoidList.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/HProp.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Option.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Sigma/Related.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/ListUtil/Forall.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/OptionList.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/LetIn.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Sigma.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Harness.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/DestructHead.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/DebugPrint.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/PrimitiveHList.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Comparison.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Notations.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/String.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/PreCommon.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersGenerateProofs.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Logic/ExistsEqAnd.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/ParseArithmetic.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Pointed.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/FixCoqMistakes.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/UnderLets.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Decidable.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Prod.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/definition_by_tactic_plugin.cmxa../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/CacheTerm.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/LetIn.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/PrimitiveSigma.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Sum.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersGenerateProofs.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Logic/ExistsEqAnd.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/inductive_from_elim_plugin.cmxa../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/rewriter_build.cmx../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Bool/Equality.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/strategy_tactic_plugin.cmxa../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Equality.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/PrimitiveProd.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Bool.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/RewriteHyp.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SplitInContext.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/CPSId.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/CPSNotations.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/Parse/Common.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/InductiveHList.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/IffT.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/IdentifiersBasicLibrary.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/DestructHyps.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/Pre.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SetoidSubst.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/TypeList.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/HProp.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/definition_by_tactic_plugin.cmx../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SpecializeBy.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/strategy_tactic_plugin.cmx../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/strategy_tactic_plugin.cmi../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/definition_by_tactic_plugin.cmi../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/definition_by_tactic.cmx../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/Decimal.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/ListUtil/SetoidList.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Isomorphism.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/inductive_from_elim_plugin.cmx../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/rewriter_build_plugin.cmx../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/BreakMatch.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/inductive_from_elim_plugin.cmi../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/rewriter_build_plugin.cmi../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/HeadUnderBinders.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/CPSNotations.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/UniquePose.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/definition_by_tactic.cmi../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/DestructHead.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/inductive_from_elim.cmx../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/PrimitiveHList.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/FindHyp.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/DoWithHyp.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/MSetPositive/Facts.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Logic/ProdForall.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/FixCoqMistakes.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/rewriter_build.cmi../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/RunTacticAsConstr.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/Pre.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/FixCoqMistakes.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/DebugPrint.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/PreLemmas.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/strategy_tactic.cmx../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/inductive_from_elim.cmi../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/FMapPositive/Equality.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SpecializeAllWays.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/TransparentAssert.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PrefixSums.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/AssertSucceedsPreserveError.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/Head.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/LetIn.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/strategy_tactic.cmi../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Pointed.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Sigma/Related.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/PrintContext.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/OptionList.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/HProp.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Demo.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/InductiveHList.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/CacheTerm.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/Ascii.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/DebugPrint.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/WarnIfGoalsRemain.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Demo.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/PrintGoal.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/ConstrFail.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/Contains.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/CPSNotations.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/Not.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SubstEvars.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/EvarNormalize.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SetEvars.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/Test.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/CPSId.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/StrategyTactic.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/GetGoal.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/DestructHyps.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/PreCommon.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Logic/ProdForall.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/GlobalSettings.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SplitInContext.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/Decimal.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SplitInContext.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Logic/ExistsEqAnd.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/MSetPositive/Facts.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/CPSId.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Isomorphism.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/TypeList.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuildRegistry.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SpecializeBy.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Isomorphism.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/MSetPositive/Equality.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/UniquePose.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/DestructHead.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Language/PreCommon.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/IffT.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/BreakMatch.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/FMapPositive/Equality.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/FindHyp.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SetoidSubst.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/GlobalSettings.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Strings/Ascii.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/StrategyTactic.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/HeadUnderBinders.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/InductiveHList.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/TransparentAssert.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/PrimitiveHList.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/RunTacticAsConstr.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/CacheTerm.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuildRegistryImports.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/DoWithHyp.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/TypeList.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuild.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/MSetPositive/Equality.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/IffT.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/ConstrFail.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuildRegistryImports.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/HeadUnderBinders.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/PrintContext.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Settings.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SpecializeBy.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Rewriter/Examples/PerfTesting/Settings.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/RunTacticAsConstr.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuild.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/Contains.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SpecializeAllWays.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/AssertSucceedsPreserveError.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/Not.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/WarnIfGoalsRemain.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/Head.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/PrintGoal.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/Test.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SpecializeAllWays.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/PrintContext.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/EvarNormalize.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Notations.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/DoWithHyp.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Logic/ProdForall.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/RewriteHyp.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/UniquePose.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/RewriterBuildRegistry.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Bool/Equality.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/AssertSucceedsPreserveError.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SetEvars.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/WarnIfGoalsRemain.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/PrintGoal.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SetoidSubst.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/DestructHyps.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/FindHyp.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/Head.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/Not.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Comparison.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SubstEvars.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/TransparentAssert.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/EvarNormalize.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/plugins/StrategyTactic.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SubstEvars.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/ConstrFail.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/SetEvars.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/Contains.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/GetGoal.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/GlobalSettings.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/Test.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Bool/Equality.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Tactics/GetGoal.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/Rewriter/Util/Comparison.vopam remove -y coq-rewriter.0.0.2