diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | tactics/hipattern.ml (renamed from tactics/hipattern.ml4) | 0 |
2 files changed, 0 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore index 06cac2fee..55df76e30 100644 --- a/.gitignore +++ b/.gitignore @@ -126,7 +126,6 @@ grammar/tacextend.ml grammar/vernacextend.ml grammar/argextend.ml parsing/cLexer.ml -tactics/hipattern.ml ltac/coretactics.ml ltac/extratactics.ml ltac/extraargs.ml diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml index 51d4c1635..51d4c1635 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml |