-R src/Rewriter Rewriter
-I src/Rewriter/Util/plugins
-arg -w -arg +implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern
src/Rewriter/Demo.v
src/Rewriter/Language/IdentifiersBasicGenerate.v
src/Rewriter/Language/IdentifiersBasicLibrary.v
src/Rewriter/Language/IdentifiersGenerate.v
src/Rewriter/Language/IdentifiersGenerateProofs.v
src/Rewriter/Language/IdentifiersLibrary.v
src/Rewriter/Language/IdentifiersLibraryProofs.v
src/Rewriter/Language/Inversion.v
src/Rewriter/Language/Language.v
src/Rewriter/Language/Pre.v
src/Rewriter/Language/PreCommon.v
src/Rewriter/Language/PreLemmas.v
src/Rewriter/Language/UnderLets.v
src/Rewriter/Language/UnderLetsProofs.v
src/Rewriter/Language/Wf.v
src/Rewriter/Rewriter/AllTactics.v
src/Rewriter/Rewriter/Examples.v
src/Rewriter/Rewriter/InterpProofs.v
src/Rewriter/Rewriter/ProofsCommon.v
src/Rewriter/Rewriter/ProofsCommonTactics.v
src/Rewriter/Rewriter/Reify.v
src/Rewriter/Rewriter/Rewriter.v
src/Rewriter/Rewriter/Wf.v
src/Rewriter/Rewriter/Examples/LiftLetsMap.v
src/Rewriter/Rewriter/Examples/Plus0Tree.v
src/Rewriter/Rewriter/Examples/PrefixSums.v
src/Rewriter/Rewriter/Examples/SieveOfEratosthenes.v
src/Rewriter/Rewriter/Examples/UnderLetsPlus0.v
src/Rewriter/Rewriter/Examples/PerfTesting/All.v
src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v
src/Rewriter/Rewriter/Examples/PerfTesting/Settings.v
src/Rewriter/Util/Bool.v
src/Rewriter/Util/CPSNotations.v
src/Rewriter/Util/Comparison.v
src/Rewriter/Util/Decidable.v
src/Rewriter/Util/Equality.v
src/Rewriter/Util/FixCoqMistakes.v
src/Rewriter/Util/GlobalSettings.v
src/Rewriter/Util/HProp.v
src/Rewriter/Util/IffT.v
src/Rewriter/Util/InductiveHList.v
src/Rewriter/Util/Isomorphism.v
src/Rewriter/Util/LetIn.v
src/Rewriter/Util/ListUtil.v
src/Rewriter/Util/NatUtil.v
src/Rewriter/Util/Notations.v
src/Rewriter/Util/Option.v
src/Rewriter/Util/OptionList.v
src/Rewriter/Util/Pointed.v
src/Rewriter/Util/PrimitiveHList.v
src/Rewriter/Util/PrimitiveProd.v
src/Rewriter/Util/PrimitiveSigma.v
src/Rewriter/Util/Prod.v
src/Rewriter/Util/Sigma.v
src/Rewriter/Util/Sum.v
src/Rewriter/Util/TypeList.v
src/Rewriter/Util/Bool/Equality.v
src/Rewriter/Util/Bool/Reflect.v
src/Rewriter/Util/FMapPositive/Equality.v
src/Rewriter/Util/ListUtil/Forall.v
src/Rewriter/Util/ListUtil/SetoidList.v
src/Rewriter/Util/Logic/ExistsEqAnd.v
src/Rewriter/Util/Logic/ProdForall.v
src/Rewriter/Util/MSetPositive/Equality.v
src/Rewriter/Util/MSetPositive/Facts.v
src/Rewriter/Util/Sigma/Related.v
src/Rewriter/Util/Tactics/AssertSucceedsPreserveError.v
src/Rewriter/Util/Tactics/BreakMatch.v
src/Rewriter/Util/Tactics/CPSId.v
src/Rewriter/Util/Tactics/CacheTerm.v
src/Rewriter/Util/Tactics/ConstrFail.v
src/Rewriter/Util/Tactics/DebugPrint.v
src/Rewriter/Util/Tactics/DestructHead.v
src/Rewriter/Util/Tactics/DestructHyps.v
src/Rewriter/Util/Tactics/DoWithHyp.v
src/Rewriter/Util/Tactics/EvarNormalize.v
src/Rewriter/Util/Tactics/GetGoal.v
src/Rewriter/Util/Tactics/Head.v
src/Rewriter/Util/Tactics/HeadUnderBinders.v
src/Rewriter/Util/Tactics/Not.v
src/Rewriter/Util/Tactics/PrintContext.v
src/Rewriter/Util/Tactics/PrintGoal.v
src/Rewriter/Util/Tactics/RewriteHyp.v
src/Rewriter/Util/Tactics/RunTacticAsConstr.v
src/Rewriter/Util/Tactics/SetEvars.v
src/Rewriter/Util/Tactics/SpecializeAllWays.v
src/Rewriter/Util/Tactics/SpecializeBy.v
src/Rewriter/Util/Tactics/SplitInContext.v
src/Rewriter/Util/Tactics/SubstEvars.v
src/Rewriter/Util/Tactics/Test.v
src/Rewriter/Util/Tactics/TransparentAssert.v
src/Rewriter/Util/Tactics/UniquePose.v
src/Rewriter/Util/Tactics/WarnIfGoalsRemain.v
src/Rewriter/Util/plugins/RewriterBuild.v
src/Rewriter/Util/plugins/RewriterBuildRegistryImports.v
src/Rewriter/Util/plugins/StrategyTactic.v
src/Rewriter/Util/plugins/definition_by_tactic.ml
src/Rewriter/Util/plugins/definition_by_tactic.mli
src/Rewriter/Util/plugins/definition_by_tactic_plugin.@ML4_OR_MLG@
src/Rewriter/Util/plugins/definition_by_tactic_plugin.mllib
src/Rewriter/Util/plugins/inductive_from_elim.ml
src/Rewriter/Util/plugins/inductive_from_elim.mli
src/Rewriter/Util/plugins/inductive_from_elim_plugin.@ML4_OR_MLG@
src/Rewriter/Util/plugins/inductive_from_elim_plugin.mllib
src/Rewriter/Util/plugins/rewriter_build.ml
src/Rewriter/Util/plugins/rewriter_build.mli
src/Rewriter/Util/plugins/rewriter_build_plugin.@ML4_OR_MLG@
src/Rewriter/Util/plugins/rewriter_build_plugin.mllib
src/Rewriter/Util/plugins/strategy_tactic.ml
src/Rewriter/Util/plugins/strategy_tactic.mli
src/Rewriter/Util/plugins/strategy_tactic_plugin.@ML4_OR_MLG@
src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib
src/Rewriter/Util/plugins/RewriterBuildRegistry.v