diff options
| author | Pierre Letouzey | 2014-03-01 19:50:59 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-03-02 20:00:02 +0100 |
| commit | 4b68dbe3428740a61cda825d3a45047571d9f299 (patch) | |
| tree | 487dff0e37d819e7de07196eac6f4699f8ab1f96 /grammar | |
| parent | 412f848e681e3c94c635f65638310a13d675449e (diff) | |
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
NB: new file miscprint.ml deserves to be part of printing.cma,
but should be part of proofs.cma for the moment, due to use in logic.ml
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/grammar.mllib | 28 |
1 files changed, 15 insertions, 13 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index b1c1c3c8e7..3f5fc5e863 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -11,7 +11,6 @@ Pp_control Flags Pp Loc -Compat Errors Hashset Hashcons @@ -25,30 +24,33 @@ Predicate Segmenttree Unicodetable Unicode +Genarg Evar Names + Libnames -Genarg + +Redops +Miscops +Locusops + Stdarg Constrarg +Constrexpr_ops + +Compat Tok Lexer Pcoq +G_prim +G_tactic +G_ltac +G_constr + Q_util Q_coqast Egramml Argextend Tacextend Vernacextend - -Nameops -Redops -Miscops -Glob_ops -Constrexpr_ops -Locusops -G_prim -G_tactic -G_ltac -G_constr |