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
---
 plugins/funind/g_indfun.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index ca90b37593..cc9ae912dc 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -78,7 +78,8 @@ END
 
 let pr_intro_as_pat prc _ _ pat =
   match pat with
-    | Some pat -> spc () ++ str "as" ++ spc () ++ pr_intro_pattern pat
+    | Some pat ->
+      spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern pat
     | None -> mt ()
 
 
-- 
cgit v1.2.3