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