aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/.cvsignore
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/.cvsignore')
-rw-r--r--parsing/.cvsignore12
1 files changed, 0 insertions, 12 deletions
diff --git a/parsing/.cvsignore b/parsing/.cvsignore
deleted file mode 100644
index a2e50565c..000000000
--- a/parsing/.cvsignore
+++ /dev/null
@@ -1,12 +0,0 @@
-lexer.ml
-*.ppo
-pcoq.ml
-g_prim.ml
-q_coqast.ml
-g_basevernac.ml
-g_vernac.ml
-g_tactic.ml
-g_constr.ml
-g_cases.ml
-g_proofs.ml
-g_minicoq.ml