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
---
 dev/printers.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 0138f70344..82ef43a7d5 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -157,6 +157,7 @@ Modintern
 Constrextern
 Proof_type
 Goal
+Miscprint
 Logic
 Refiner
 Clenv
-- 
cgit v1.2.3