diff options
Diffstat (limited to 'parsing/parsing.mllib')
| -rw-r--r-- | parsing/parsing.mllib | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 84a08d54..a0cb8319 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,11 +1,6 @@ -Extend -Extrawit +Tok +Compat +Lexer Pcoq -Egrammar -G_xml -Ppconstr -Printer -Pptactic -Tactic_printer -Printmod -Prettyp +Egramml +Egramcoq |