diff --git a/.gitignore b/.gitignore index 804803d82..b3d517729 100644 --- a/.gitignore +++ b/.gitignore @@ -99,6 +99,7 @@ src/Rewriter/Util/plugins/ltac2_extra_plugin.ml src/Rewriter/Util/plugins/RewriterBuildRegistry.v src/Rewriter/Util/plugins/RewriterBuild.v src/Rewriter/Util/plugins/StrategyTactic.v +src/Rewriter/Util/plugins/Ltac2Extra.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