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 /printing/printer.ml | |
| 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 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 85b3c1836a..9143d1c5b3 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -647,7 +647,7 @@ let pr_prim_rule = function | Move (withdep,id1,id2) -> (str (if withdep then "dependent " else "") ++ - str"move " ++ pr_id id1 ++ Miscops.pr_move_location pr_id id2) + str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2) | Order ord -> (str"order " ++ pr_sequence pr_id ord) |