diff options
| -rw-r--r-- | doc/tools/coqrst/notations/TacticNotationsVisitor.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/coqrst/notations/TacticNotationsVisitor.py b/doc/tools/coqrst/notations/TacticNotationsVisitor.py index 80e69d4335..423b2cfe9d 100644 --- a/doc/tools/coqrst/notations/TacticNotationsVisitor.py +++ b/doc/tools/coqrst/notations/TacticNotationsVisitor.py @@ -50,4 +50,4 @@ class TacticNotationsVisitor(ParseTreeVisitor): -del TacticNotationsParser
\ No newline at end of file +del TacticNotationsParser |