diff options
| -rw-r--r-- | grammar/grammar.mllib | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index fc7cb392bf..296d32dc04 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -29,35 +29,22 @@ CStack Util Ppstyle Errors -Bigint Predicate Segmenttree Unicodetable Unicode Genarg -Evar Names -Libnames - -Redops -Miscops -Locusops - Stdarg Constrarg -Constrexpr_ops Tok Compat Lexer Entry Pcoq -G_prim -G_tactic -G_ltac -G_constr Q_util Egramml |