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 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 1 |
2 files changed, 2 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 68be51d9c5..1116410dc2 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -279,7 +279,7 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = (first, d::middle) else errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++ - Miscops.pr_move_location pr_id hto ++ + Miscprint.pr_move_location pr_id hto ++ str (if toleft then ": it occurs in " else ": it depends on ") ++ pr_id hyp ++ str ".") else diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 96b9a89a3c..ab5cf52d46 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,3 +1,4 @@ +Miscprint Goal Evar_refiner Proof_using |