1 file changed
+1
-1
lines changed- Makefile.local.common+6-1
- src/Rewriter/Util/Tactics2/Constr.v.v821+48
- src/Rewriter/Util/Tactics2/DestCase.v.v821+11
- src/Rewriter/Util/Tactics2/DestProj.v.v821+11
- src/Rewriter/Util/Tactics2/Proj.v.v821+5
- src/Rewriter/Util/plugins/Ltac2Extra.v.v821+10
- src/Rewriter/Util/plugins/RewriterBuild.v.v821+10
- src/Rewriter/Util/plugins/RewriterBuildRegistry.v.v821+20
- src/Rewriter/Util/plugins/StrategyTactic.v.v821+35
- src/Rewriter/Util/plugins/definition_by_tactic.ml.v821+17
- src/Rewriter/Util/plugins/definition_by_tactic.mli.v821+11
- src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg.v821+22
- src/Rewriter/Util/plugins/definition_by_tactic_plugin.mllib.v821+2
- src/Rewriter/Util/plugins/inductive_from_elim.ml.v821+82
- src/Rewriter/Util/plugins/inductive_from_elim.mli.v821+3
- src/Rewriter/Util/plugins/inductive_from_elim_plugin.mlg.v821+17
- src/Rewriter/Util/plugins/inductive_from_elim_plugin.mllib.v821+2
- src/Rewriter/Util/plugins/ltac2_extra.ml.v821+20
- src/Rewriter/Util/plugins/ltac2_extra.mli.v821
- src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v821+1
- src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v821+2
- src/Rewriter/Util/plugins/rewriter_build.ml.v821+196
- src/Rewriter/Util/plugins/rewriter_build.mli.v821+3
- src/Rewriter/Util/plugins/rewriter_build_plugin.mlg.v821+82
- src/Rewriter/Util/plugins/rewriter_build_plugin.mllib.v821+4
- src/Rewriter/Util/plugins/strategy_tactic.ml.v821+7
- src/Rewriter/Util/plugins/strategy_tactic.mli.v821+1
- src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg.v821+18
- src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib.v821+2
0 commit comments