From 4b68dbe3428740a61cda825d3a45047571d9f299 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 1 Mar 2014 19:50:59 +0100 Subject: 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 --- proofs/proofs.mllib | 1 + 1 file changed, 1 insertion(+) (limited to 'proofs/proofs.mllib') diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 96b9a89a3..ab5cf52d4 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,3 +1,4 @@ +Miscprint Goal Evar_refiner Proof_using -- cgit v1.2.3