From 1d2dc36216ad110dcf49cf7ed2a05d2bbdd7546c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 7 Oct 2022 19:32:40 +0530 Subject: [PATCH] Add generated Ltac2Extra.v to .gitignore --- .gitignore | 1 + 1 file changed, 1 insertion(+) 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