Unplugging Pptactic from Ppvernac.

10 files changed, 204 insertions, 173 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index e50b0520b..be8390c95 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -983,7 +983,7 @@ let pr_cmp' _prc _prlc _prt = pr_cmp
 let pr_test_gen f (Test(c,x,y)) =
   Pp.(f x ++ pr_cmp c ++ f y)
 
-let pr_test = pr_test_gen (Pptactic.pr_or_var Pp.int)
+let pr_test = pr_test_gen (Pputils.pr_or_var Pp.int)
 
 let pr_test' _prc _prlc _prt = pr_test
 
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 0ec35e07b..6505a8f82 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -9,15 +9,17 @@
 open Pp
 open Genarg
 
-type ('raw, 'glb, 'top) printer = {
-  raw : 'raw -> std_ppcmds;
-  glb : 'glb -> std_ppcmds;
-  top : 'top -> std_ppcmds;
+type 'a printer = 'a -> std_ppcmds
+
+type ('raw, 'glb, 'top) genprinter = {
+  raw : 'raw printer;
+  glb : 'glb printer;
+  top : 'top printer;
 }
 
 module PrintObj =
 struct
-  type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) printer
+  type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) genprinter
   let name = "printer"
   let default wit = match wit with
   | ExtraArg tag ->
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 6e6626f2f..5381fc5bd 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -11,6 +11,8 @@
 open Pp
 open Genarg
 
+type 'a printer = 'a -> std_ppcmds
+
 val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> std_ppcmds
 (** Printer for raw level generic arguments. *)
 
@@ -20,9 +22,9 @@ val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> std_ppcmds
 val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> std_ppcmds
 (** Printer for top level generic arguments. *)
 
-val generic_raw_print : rlevel generic_argument -> std_ppcmds
-val generic_glb_print : glevel generic_argument -> std_ppcmds
-val generic_top_print : tlevel generic_argument -> std_ppcmds
+val generic_raw_print : rlevel generic_argument printer
+val generic_glb_print : glevel generic_argument printer
+val generic_top_print : tlevel generic_argument printer
 
 val register_print0 : ('raw, 'glb, 'top) genarg_type ->
-  ('raw -> std_ppcmds) -> ('glb -> std_ppcmds) -> ('top -> std_ppcmds) -> unit
+  'raw printer -> 'glb printer -> 'top printer -> unit
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 917a277c9..a4222ae2c 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -22,6 +22,7 @@ open Misctypes
 open Locus
 open Decl_kinds
 open Genredexpr
+open Pputils
 open Ppconstr
 open Printer
 
@@ -62,19 +63,6 @@ type 'a extra_genarg_printer =
     (tolerability -> Val.t -> std_ppcmds) ->
     'a -> std_ppcmds
 
-let genarg_pprule = ref String.Map.empty
-
-let declare_extra_genarg_pprule wit f g h =
-  let s = match wit with
-    | ExtraArg s -> ArgT.repr s
-    | _ -> error
-      "Can declare a pretty-printing rule only for extra argument types."
-  in
-  let f prc prlc prtac x = f prc prlc prtac (out_gen (rawwit wit) x) in
-  let g prc prlc prtac x = g prc prlc prtac (out_gen (glbwit wit) x) in
-  let h prc prlc prtac x = h prc prlc prtac (out_gen (topwit wit) x) in
-  genarg_pprule := String.Map.add s (f,g,h) !genarg_pprule
-
 module Make
   (Ppconstr : Ppconstrsig.Pp)
   (Taggers : sig
@@ -135,80 +123,8 @@ module Make
           end
         | _ -> default
 
-  let pr_with_occurrences pr (occs,c) =
-    match occs with
-      | AllOccurrences ->
-        pr c
-      | NoOccurrences ->
-        failwith "pr_with_occurrences: no occurrences"
-      | OnlyOccurrences nl ->
-        hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++
-                 hov 0 (prlist_with_sep spc (pr_or_var int) nl))
-      | AllOccurrencesBut nl ->
-        hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
-                 hov 0 (prlist_with_sep spc (pr_or_var int) nl))
-
-  exception ComplexRedFlag
-
-  let pr_short_red_flag pr r =
-    if not r.rBeta ||  not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then
-      raise ComplexRedFlag
-    else if List.is_empty r.rConst then
-      if r.rDelta then mt () else raise ComplexRedFlag
-    else (if r.rDelta then str "-" else mt ()) ++
-	   hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")
-
-  let pr_red_flag pr r =
-    try pr_short_red_flag pr r
-    with complexRedFlags ->
-      (if r.rBeta then pr_arg str "beta" else mt ()) ++
-	(if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else
-           (if r.rMatch then pr_arg str "match" else mt ()) ++
-           (if r.rFix then pr_arg str "fix" else mt ()) ++
-           (if r.rCofix then pr_arg str "cofix" else mt ())) ++
-        (if r.rZeta then pr_arg str "zeta" else mt ()) ++
-        (if List.is_empty r.rConst then
-	   if r.rDelta then pr_arg str "delta"
-	   else mt ()
-	 else
-	   pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
-	     hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
-
-  let pr_union pr1 pr2 = function
-    | Inl a -> pr1 a
-    | Inr b -> pr2 b
-
-  let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
-    | Red false -> keyword "red"
-    | Hnf -> keyword "hnf"
-    | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
-		     ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
-    | Cbv f ->
-      if f.rBeta && f.rMatch && f.rFix && f.rCofix &&
-           f.rZeta && f.rDelta && List.is_empty f.rConst then
-        keyword "compute"
-      else
-        hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f)
-    | Lazy f ->
-      hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f)
-    | Cbn f ->
-      hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f)
-    | Unfold l ->
-      hov 1 (keyword "unfold" ++ spc() ++
-               prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l)
-    | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l)
-    | Pattern l ->
-      hov 1 (keyword "pattern" ++
-               pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr)) l)
-
-    | Red true ->
-      error "Shouldn't be accessible from user."
-    | ExtraRedExpr s ->
-      str s
-    | CbvVm o ->
-      keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
-    | CbvNative o ->
-      keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
+  let pr_with_occurrences pr c = pr_with_occurrences pr keyword c
+  let pr_red_expr pr c = pr_red_expr pr keyword c
 
   let pr_may_eval test prc prlc pr2 pr3 = function
     | ConstrEval (r,c) ->
@@ -232,10 +148,6 @@ module Make
 
   let pr_arg pr x = spc () ++ pr x
 
-  let pr_or_var pr = function
-    | ArgArg x -> pr x
-    | ArgVar (_,s) -> pr_id s
-
   let pr_and_short_name pr (c,_) = pr c
 
   let pr_or_by_notation f = function
@@ -300,52 +212,6 @@ module Make
 
   let with_evars ev s = if ev then "e" ^ s else s
 
-  let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
-
-  let rec pr_raw_generic_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) =
-    match wit with
-      | ListArg wit ->
-        let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
-        let ans = pr_sequence map x in
-        hov_if_not_empty 0 ans
-      | OptArg wit ->
-        let ans = match x with
-          | None -> mt ()
-          | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x)
-        in
-        hov_if_not_empty 0 ans
-      | PairArg (wit1, wit2) ->
-        let p, q = x in
-        let p = in_gen (rawwit wit1) p in
-        let q = in_gen (rawwit wit2) q in
-        hov_if_not_empty 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q])
-      | ExtraArg s ->
-        try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x)
-        with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x)
-
-
-  let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) =
-    match wit with
-      | ListArg wit ->
-        let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in
-        let ans = pr_sequence map x in
-        hov_if_not_empty 0 ans
-      | OptArg wit ->
-        let ans = match x with
-          | None -> mt ()
-          | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x)
-        in
-        hov_if_not_empty 0 ans
-      | PairArg (wit1, wit2) ->
-        let p, q = x in
-        let p = in_gen (glbwit wit1) p in
-        let q = in_gen (glbwit wit2) q in
-        let ans = pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q] in
-        hov_if_not_empty 0 ans
-      | ExtraArg s ->
-        try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x)
-        with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x)
-
   let rec tacarg_using_rule_token pr_gen = function
     | [] -> []
     | TacTerm s :: l -> keyword s :: tacarg_using_rule_token pr_gen l
@@ -1227,7 +1093,7 @@ module Make
       pr_constant = pr_or_by_notation pr_reference;
       pr_reference = pr_reference;
       pr_name = pr_lident;
-      pr_generic = pr_raw_generic_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference;
+      pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg);
       pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
       pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
     } in
@@ -1257,9 +1123,7 @@ module Make
         pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
         pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
         pr_name = pr_lident;
-        pr_generic = pr_glb_generic_rec
-          (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
-          prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
+        pr_generic = (fun arg -> Pputils.pr_glb_generic (Global.env ()) arg);
         pr_extend = pr_glob_extend_rec
           (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
           prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
@@ -1307,12 +1171,9 @@ module Make
     in
     prtac n t
 
-  let pr_raw_generic env = pr_raw_generic_rec
-    pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference
+  let pr_raw_generic = Pputils.pr_raw_generic
 
-  let pr_glb_generic env = pr_glb_generic_rec
-    (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
-    (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+  let pr_glb_generic = Pputils.pr_glb_generic
 
   let pr_raw_extend env = pr_raw_extend_rec
     pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
@@ -1360,6 +1221,26 @@ include Make (Ppconstr) (struct
     let tag_atomic_tactic_expr      = do_not_tag
 end)
 
+let declare_extra_genarg_pprule wit
+  (f : 'a raw_extra_genarg_printer)
+  (g : 'b glob_extra_genarg_printer)
+  (h : 'c extra_genarg_printer) =
+  let s = match wit with
+    | ExtraArg s -> ArgT.repr s
+    | _ -> error
+      "Can declare a pretty-printing rule only for extra argument types."
+  in
+  let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
+  let g x =
+    let env = Global.env () in
+    g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x
+  in
+  let h x =
+    let env = Global.env () in
+    h (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x
+  in
+  Genprint.register_print0 wit f g h
+
 (** Registering *)
 
 let run_delayed c =
@@ -1413,7 +1294,7 @@ let () =
   ;
   Genprint.register_print0 Constrarg.wit_red_expr
     (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
-    (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
+    (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
     (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern));
   Genprint.register_print0 Constrarg.wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
   Genprint.register_print0 Constrarg.wit_bindings
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index c08d6044d..455cc1be1 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -25,9 +25,7 @@ module type Pp = sig
     ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
     ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
 
-  val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
   val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
-  val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
 
   val pr_clauses :  bool option ->
     ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 906b463a8..33382fe83 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -6,10 +6,143 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Pp
+open Genarg
+open Nameops
+open Misctypes
+open Locus
+open Genredexpr
 
 let pr_located pr (loc, x) =
   if Flags.do_beautify () && loc <> Loc.ghost then
     let (b, e) = Loc.unloc loc in
     Pp.comment b ++ pr x ++ Pp.comment e
   else pr x
+
+let pr_or_var pr = function
+  | ArgArg x -> pr x
+  | ArgVar (_,s) -> pr_id s
+
+let pr_with_occurrences pr keyword (occs,c) =
+  match occs with
+    | AllOccurrences ->
+      pr c
+    | NoOccurrences ->
+      failwith "pr_with_occurrences: no occurrences"
+    | OnlyOccurrences nl ->
+      hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++
+                hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+    | AllOccurrencesBut nl ->
+      hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
+                hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+
+exception ComplexRedFlag
+
+let pr_short_red_flag pr r =
+  if not r.rBeta ||  not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then
+    raise ComplexRedFlag
+  else if List.is_empty r.rConst then
+    if r.rDelta then mt () else raise ComplexRedFlag
+  else (if r.rDelta then str "-" else mt ()) ++
+          hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")
+
+let pr_red_flag pr r =
+  try pr_short_red_flag pr r
+  with complexRedFlags ->
+    (if r.rBeta then pr_arg str "beta" else mt ()) ++
+      (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else
+          (if r.rMatch then pr_arg str "match" else mt ()) ++
+          (if r.rFix then pr_arg str "fix" else mt ()) ++
+          (if r.rCofix then pr_arg str "cofix" else mt ())) ++
+      (if r.rZeta then pr_arg str "zeta" else mt ()) ++
+      (if List.is_empty r.rConst then
+          if r.rDelta then pr_arg str "delta"
+          else mt ()
+        else
+          pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
+            hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
+
+let pr_union pr1 pr2 = function
+  | Inl a -> pr1 a
+  | Inr b -> pr2 b
+
+let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
+  | Red false -> keyword "red"
+  | Hnf -> keyword "hnf"
+  | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
+                    ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+  | Cbv f ->
+    if f.rBeta && f.rMatch && f.rFix && f.rCofix &&
+          f.rZeta && f.rDelta && List.is_empty f.rConst then
+      keyword "compute"
+    else
+      hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f)
+  | Lazy f ->
+    hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f)
+  | Cbn f ->
+    hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f)
+  | Unfold l ->
+    hov 1 (keyword "unfold" ++ spc() ++
+              prlist_with_sep pr_comma (pr_with_occurrences pr_ref keyword) l)
+  | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l)
+  | Pattern l ->
+    hov 1 (keyword "pattern" ++
+              pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l)
+
+  | Red true ->
+    CErrors.error "Shouldn't be accessible from user."
+  | ExtraRedExpr s ->
+    str s
+  | CbvVm o ->
+    keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+  | CbvNative o ->
+    keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+
+let pr_or_by_notation f = function
+  | AN v -> f v
+  | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+
+let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
+
+let rec pr_raw_generic env (GenArg (Rawwit wit, x)) =
+  match wit with
+    | ListArg wit ->
+      let map x = pr_raw_generic env (in_gen (rawwit wit) x) in
+      let ans = pr_sequence map x in
+      hov_if_not_empty 0 ans
+    | OptArg wit ->
+      let ans = match x with
+        | None -> mt ()
+        | Some x -> pr_raw_generic env (in_gen (rawwit wit) x)
+      in
+      hov_if_not_empty 0 ans
+    | PairArg (wit1, wit2) ->
+      let p, q = x in
+      let p = in_gen (rawwit wit1) p in
+      let q = in_gen (rawwit wit2) q in
+      hov_if_not_empty 0 (pr_sequence (pr_raw_generic env) [p; q])
+    | ExtraArg s ->
+      Genprint.generic_raw_print (in_gen (rawwit wit) x)
+
+
+let rec pr_glb_generic env (GenArg (Glbwit wit, x)) =
+  match wit with
+    | ListArg wit ->
+      let map x = pr_glb_generic env (in_gen (glbwit wit) x) in
+      let ans = pr_sequence map x in
+      hov_if_not_empty 0 ans
+    | OptArg wit ->
+      let ans = match x with
+        | None -> mt ()
+        | Some x -> pr_glb_generic env (in_gen (glbwit wit) x)
+      in
+      hov_if_not_empty 0 ans
+    | PairArg (wit1, wit2) ->
+      let p, q = x in
+      let p = in_gen (glbwit wit1) p in
+      let q = in_gen (glbwit wit2) q in
+      let ans = pr_sequence (pr_glb_generic env) [p; q] in
+      hov_if_not_empty 0 ans
+    | ExtraArg s ->
+      Genprint.generic_glb_print (in_gen (glbwit wit) x)
diff --git a/printing/pputils.mli b/printing/pputils.mli
index a0f2c7728..b236fed70 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -7,7 +7,25 @@
 (************************************************************************)
 
 open Pp
+open Genarg
+open Misctypes
+open Locus
+open Genredexpr
 
 val pr_located : ('a -> std_ppcmds) -> 'a Loc.located -> std_ppcmds
 (** Prints an object surrounded by its commented location *)
 
+val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
+val pr_with_occurrences :
+  ('a -> std_ppcmds) -> (string -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
+
+val pr_short_red_flag : ('a -> std_ppcmds) -> 'a glob_red_flag -> std_ppcmds
+val pr_red_flag : ('a -> std_ppcmds) -> 'a glob_red_flag -> std_ppcmds
+val pr_red_expr :
+  ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
+  (string -> std_ppcmds) ->
+  ('a,'b,'c) red_expr_gen -> std_ppcmds
+
+val pr_raw_generic : Environ.env -> rlevel generic_argument -> std_ppcmds
+val pr_glb_generic : Environ.env -> glevel generic_argument -> std_ppcmds
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index d4de05da8..51fc289b4 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -21,7 +21,6 @@ open Decl_kinds
 
 module Make
   (Ppconstr : Ppconstrsig.Pp)
-  (Pptactic : Pptacticsig.Pp)
   (Taggers  : sig
     val tag_keyword : std_ppcmds -> std_ppcmds
     val tag_vernac  : vernac_expr -> std_ppcmds -> std_ppcmds
@@ -30,7 +29,6 @@ module Make
 
   open Taggers
   open Ppconstr
-  open Pptactic
 
   let keyword s = tag_keyword (str s)
 
@@ -67,7 +65,7 @@ module Make
     | (loc,Name id) -> pr_lident (loc,id)
     | lna -> pr_located pr_name lna
 
-  let pr_smart_global = pr_or_by_notation pr_reference
+  let pr_smart_global = Pputils.pr_or_by_notation pr_reference
 
   let pr_ltac_ref = Libnames.pr_reference
 
@@ -81,7 +79,7 @@ module Make
     | VernacEndSubproof -> str""
     | _ -> str"."
 
-  let pr_gen t = pr_raw_generic (Global.env ()) t
+  let pr_gen t = Pputils.pr_raw_generic (Global.env ()) t
 
   let sep = fun _ -> spc()
   let sep_v2 = fun _ -> str"," ++ spc()
@@ -195,7 +193,7 @@ module Make
         | HintsExtern (n,c,tac) ->
           let pat = match c with None -> mt () | Some pat -> pr_pat pat in
           keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
-            spc() ++ pr_raw_generic (Global.env ()) tac
+            spc() ++ Pputils.pr_raw_generic (Global.env ()) tac
     in
     hov 2 (keyword "Hint "++ pph ++ opth)
 
@@ -703,7 +701,7 @@ module Make
           | None -> mt()
           | Some r ->
             keyword "Eval" ++ spc() ++
-              pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++
+              pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
               keyword " in" ++ spc()
         in
         let pr_def_body = function
@@ -1127,7 +1125,7 @@ module Make
         let pr_mayeval r c = match r with
           | Some r0 ->
             hov 2 (keyword "Eval" ++ spc() ++
-                     pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++
+                     pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
                      spc() ++ keyword "in" ++ spc () ++ pr_lconstr c)
           | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
         in
@@ -1138,7 +1136,7 @@ module Make
       | VernacDeclareReduction (s,r) ->
         return (
           keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++
-            pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r
+            pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
         )
       | VernacPrint p ->
         return (pr_printable p)
@@ -1179,12 +1177,12 @@ module Make
         return (keyword "Proof " ++ spc () ++
             keyword "using" ++ spc() ++ pr_using e)
       | VernacProof (Some te, None) ->
-        return (keyword "Proof with" ++ spc() ++ pr_raw_generic (Global.env ()) te)
+        return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te)
       | VernacProof (Some te, Some e) ->
         return (
           keyword "Proof" ++ spc () ++
             keyword "using" ++ spc() ++ pr_using e ++ spc() ++
-            keyword "with" ++ spc() ++ pr_raw_generic (Global.env ()) te
+            keyword "with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te
         )
       | VernacProofMode s ->
         return (keyword "Proof Mode" ++ str s)
@@ -1223,7 +1221,7 @@ module Make
 
 end
 
-include Make (Ppconstr) (Pptactic) (struct
+include Make (Ppconstr) (struct
   let do_not_tag _ x = x
   let tag_keyword = do_not_tag ()
   let tag_vernac  = do_not_tag
@@ -1233,7 +1231,6 @@ module Richpp = struct
 
   include Make
     (Ppconstr.Richpp)
-    (Pptactic.Richpp)
     (struct
       open Ppannotation
       let tag_keyword s = Pp.tag (Pp.Tag.inj AKeyword tag) s
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 7628b7885..dae1cc9f1 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -83,7 +83,7 @@ let print_rewrite_hintdb bas =
 	     str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
 	       Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
 	       Option.cata (fun tac -> str " then use tactic " ++
-	       Pptactic.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac)
+	       Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac)
 	   (find_rewrites bas))
 
 type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option
diff --git a/tactics/hints.ml b/tactics/hints.ml
index a6d1fc6c8..4be4d1ed4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1276,7 +1276,7 @@ let pr_hint h = match h.obj with
           env
         with e when CErrors.noncritical e -> Global.env ()
       in
-      (str "(*external*) " ++ Pptactic.pr_glb_generic env tac)
+      (str "(*external*) " ++ Pputils.pr_glb_generic env tac)
 
 let pr_id_hint (id, v) =
   (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())