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

4 files changed, 73 insertions, 10 deletions

diff --git a/printing/miscprint.ml b/printing/miscprint.ml
new file mode 100644
index 0000000000..3a0f7a8f75
--- /dev/null
+++ b/printing/miscprint.ml
@@ -0,0 +1,41 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Misctypes
+open Pp
+
+(** Printing of [intro_pattern] *)
+
+let rec pr_intro_pattern (_,pat) = match pat with
+  | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll
+  | IntroInjection pl ->
+      str "[=" ++ hv 0 (prlist_with_sep spc pr_intro_pattern pl) ++ str "]"
+  | IntroWildcard -> str "_"
+  | IntroRewrite true -> str "->"
+  | IntroRewrite false -> str "<-"
+  | IntroIdentifier id -> Nameops.pr_id id
+  | IntroFresh id -> str "?" ++ Nameops.pr_id id
+  | IntroForthcoming true -> str "*"
+  | IntroForthcoming false -> str "**"
+  | IntroAnonymous -> str "?"
+
+and pr_or_and_intro_pattern = function
+  | [pl] ->
+      str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")"
+  | pll ->
+      str "[" ++
+      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
+      ++ str "]"
+
+(** Printing of [move_location] *)
+
+let pr_move_location pr_id = function
+  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
+  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
+  | MoveFirst -> str " at top"
+  | MoveLast -> str " at bottom"
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
new file mode 100644
index 0000000000..4e0be83f24
--- /dev/null
+++ b/printing/miscprint.mli
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Misctypes
+
+(** Printing of [intro_pattern] *)
+
+val pr_intro_pattern : intro_pattern_expr Loc.located -> Pp.std_ppcmds
+
+(** Printing of [move_location] *)
+
+val pr_move_location :
+  ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index ae3b41e231..adb2ba0d08 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -18,7 +18,6 @@ open Constrarg
 open Libnames
 open Ppextend
 open Misctypes
-open Miscops
 open Locus
 open Decl_kinds
 open Genredexpr
@@ -342,8 +341,8 @@ let pr_bindings prlc prc = pr_bindings_gen false prlc prc
 let pr_with_bindings prlc prc (c,bl) =
   hov 1 (prc c ++ pr_bindings prlc prc bl)
 
-let pr_as_ipat pat = str "as " ++ pr_intro_pattern pat
-let pr_eqn_ipat pat = str "eqn:" ++ pr_intro_pattern pat
+let pr_as_ipat pat = str "as " ++ Miscprint.pr_intro_pattern pat
+let pr_eqn_ipat pat = str "eqn:" ++ Miscprint.pr_intro_pattern pat
 
 let pr_with_induction_names = function
   | None, None -> mt ()
@@ -353,7 +352,7 @@ let pr_with_induction_names = function
     spc () ++ hov 1 (pr_as_ipat ipat ++ spc () ++ pr_eqn_ipat eqpat)
 
 let pr_as_intro_pattern ipat =
-  spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
+  spc () ++ hov 1 (str "as" ++ spc () ++ Miscprint.pr_intro_pattern ipat)
 
 let pr_with_inversion_names = function
   | None -> mt ()
@@ -645,13 +644,15 @@ and pr_atom1 = function
   (* Basic tactics *)
   | TacIntroPattern [] as t -> pr_atom0 t
   | TacIntroPattern (_::_ as p) ->
-      hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p)
+      hov 1 (str "intros" ++ spc () ++
+             prlist_with_sep spc Miscprint.pr_intro_pattern p)
   | TacIntrosUntil h ->
       hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h)
   | TacIntroMove (None,MoveLast) as t -> pr_atom0 t
   | TacIntroMove (Some id,MoveLast) -> str "intro " ++ pr_id id
   | TacIntroMove (ido,hto) ->
-      hov 1 (str"intro" ++ pr_opt pr_id ido ++ Miscops.pr_move_location pr_ident hto)
+      hov 1 (str"intro" ++ pr_opt pr_id ido ++
+             Miscprint.pr_move_location pr_ident hto)
   | TacAssumption as t -> pr_atom0 t
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
   | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
@@ -764,7 +765,7 @@ and pr_atom1 = function
       assert b;
       hov 1
         (str "move" ++ brk (1,1) ++ pr_ident id1 ++
-	 Miscops.pr_move_location pr_ident id2)
+	 Miscprint.pr_move_location pr_ident id2)
   | TacRename l ->
       hov 1
         (str "rename" ++ brk (1,1) ++
@@ -1033,8 +1034,11 @@ let () =
   let pr_string s = str "\"" ++ str s ++ str "\"" in
   Genprint.register_print0 Constrarg.wit_ref
     pr_reference (pr_or_var (pr_located pr_global)) pr_global;
-  Genprint.register_print0 Constrarg.wit_intro_pattern
-    pr_intro_pattern pr_intro_pattern pr_intro_pattern;
+  Genprint.register_print0
+    Constrarg.wit_intro_pattern
+    Miscprint.pr_intro_pattern
+    Miscprint.pr_intro_pattern
+    Miscprint.pr_intro_pattern;
   Genprint.register_print0 Constrarg.wit_sort
     pr_glob_sort pr_glob_sort pr_sort;
   Genprint.register_print0 Stdarg.wit_int int int int;
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)