diff options
| author | Pierre-Marie Pédrot | 2016-03-06 23:15:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-06 23:19:33 +0100 |
| commit | a9f6f401e66c0bbf0c50801d597cd18097bf91a6 (patch) | |
| tree | f867ef6ff857a18554131dd1f0f85df30e25c6d3 | |
| parent | ffac73b8f3f3bf6877ce652eecac7849b7c2a182 (diff) | |
Expurging grammar.mllib from uselessly linked modules.
| -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 |