@META@
-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,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality,+future-coercion-class-field,unsupported-attributes
-arg -native-compiler -arg ondemand
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/Reify.v
src/Rewriter/Language/UnderLets.v
src/Rewriter/Language/UnderLetsCacheProofs.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/PrefixSums.v
src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v
src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v
src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v
src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v
src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v
src/Rewriter/Rewriter/Examples/PerfTesting/Settings.v
src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v
src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.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/Strings/Ascii.v
src/Rewriter/Util/Strings/Decimal.v
src/Rewriter/Util/Strings/ParseArithmetic.v
src/Rewriter/Util/Strings/String.v
src/Rewriter/Util/Strings/Parse/Common.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/ClearFree.v
src/Rewriter/Util/Tactics/ConstrFail.v
src/Rewriter/Util/Tactics/Contains.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/FindHyp.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/SetoidSubst.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/Tactics2/Array.v
src/Rewriter/Util/Tactics2/Char.v
src/Rewriter/Util/Tactics2/Constr.v
src/Rewriter/Util/Tactics2/DecomposeLambda.v
src/Rewriter/Util/Tactics2/DestApp.v
src/Rewriter/Util/Tactics2/DestCase.v
src/Rewriter/Util/Tactics2/DestCast.v
src/Rewriter/Util/Tactics2/DestCoFix.v
src/Rewriter/Util/Tactics2/DestConstant.v
src/Rewriter/Util/Tactics2/DestConstructor.v
src/Rewriter/Util/Tactics2/DestEvar.v
src/Rewriter/Util/Tactics2/DestFix.v
src/Rewriter/Util/Tactics2/DestInd.v
src/Rewriter/Util/Tactics2/DestLambda.v
src/Rewriter/Util/Tactics2/DestLetIn.v
src/Rewriter/Util/Tactics2/DestMeta.v
src/Rewriter/Util/Tactics2/DestProd.v
src/Rewriter/Util/Tactics2/DestProj.v
src/Rewriter/Util/Tactics2/DestRel.v
src/Rewriter/Util/Tactics2/DestSort.v
src/Rewriter/Util/Tactics2/DestVar.v
src/Rewriter/Util/Tactics2/FixNotationsForPerformance.v
src/Rewriter/Util/Tactics2/Head.v
src/Rewriter/Util/Tactics2/HeadReference.v
src/Rewriter/Util/Tactics2/Ident.v
src/Rewriter/Util/Tactics2/InFreshContext.v
src/Rewriter/Util/Tactics2/InstantiateEvar.v
src/Rewriter/Util/Tactics2/Iterate.v
src/Rewriter/Util/Tactics2/List.v
src/Rewriter/Util/Tactics2/Ltac1.v
src/Rewriter/Util/Tactics2/Message.v
src/Rewriter/Util/Tactics2/Notations.v
src/Rewriter/Util/Tactics2/Option.v
src/Rewriter/Util/Tactics2/Proj.v
src/Rewriter/Util/Tactics2/ReplaceByPattern.v
src/Rewriter/Util/Tactics2/String.v
src/Rewriter/Util/Tactics2/Constr/Unsafe/MakeAbbreviations.v
src/Rewriter/Util/plugins/RewriterBuildRegistryImports.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.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.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.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.mlg
src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib
src/Rewriter/Util/plugins/ltac2_extra.ml
src/Rewriter/Util/plugins/ltac2_extra.mli
src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg
src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib
src/Rewriter/Util/plugins/RewriterBuildRegistry.v
src/Rewriter/Util/plugins/RewriterBuild.v
src/Rewriter/Util/plugins/StrategyTactic.v
src/Rewriter/Util/plugins/Ltac2Extra.v