aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2015-06-23 10:12:41 +0200
committerGravatar Jason Gross <jgross@mit.edu>2016-06-05 22:09:39 -0400
commit9ff2c9d8d042c9989b6a8138c308398c49ae116f (patch)
treeab6abf0403a4db27fef257393795111284da20ae /.gitignore
parent45748e4efae8630cc13b0199dfcc9803341e8cd8 (diff)
LtacProf for Coq trunk
This add LtacProfiling. Much of the code was written by Tobias Tebbi (@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq v8.5 and Coq trunk.
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 116f88dd7..bc1a05684 100644
--- a/.gitignore
+++ b/.gitignore
@@ -128,6 +128,7 @@ parsing/cLexer.ml
ltac/coretactics.ml
ltac/extratactics.ml
ltac/extraargs.ml
+ltac/profile_ltac_tactics.ml
ide/coqide_main.ml
# other auto-generated files