printing/Pptactic.Make: New.

       - Functorize with respect to the pretty-printer for constr.
       - Include the application of Make to Ppconstr at toplevel in order to preserve
         previous behavior.

1 files changed, 995 insertions, 985 deletions

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index cb64c712dd..645a3409e4 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -24,1099 +24,1109 @@ open Genredexpr
 open Ppconstr
 open Printer
 
-let pr_global x = Nametab.pr_global_env Id.Set.empty x
+module Make (Ppconstr : Ppconstrsig.Pp) =
+struct
 
-type grammar_terminals = string option list
+  let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
-type pp_tactic = {
-  pptac_args : argument_type list;
-  pptac_prods : int * grammar_terminals;
-}
+  type grammar_terminals = string option list
 
-(* ML Extensions *)
-let prtac_tab = Hashtbl.create 17
+  type pp_tactic = {
+    pptac_args : argument_type list;
+    pptac_prods : int * grammar_terminals;
+  }
 
-(* Tactic notations *)
-let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
+  (* ML Extensions *)
+  let prtac_tab = Hashtbl.create 17
 
-let declare_ml_tactic_pprule key pt =
-  Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods
+  (* Tactic notations *)
+  let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
 
-let declare_notation_tactic_pprule kn pt =
-  prnotation_tab := KNmap.add kn pt !prnotation_tab
+  let declare_ml_tactic_pprule key pt =
+    Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods
 
-type 'a raw_extra_genarg_printer =
-    (constr_expr -> std_ppcmds) ->
-    (constr_expr -> std_ppcmds) ->
-    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
-    'a -> std_ppcmds
+  let declare_notation_tactic_pprule kn pt =
+    prnotation_tab := KNmap.add kn pt !prnotation_tab
 
-type 'a glob_extra_genarg_printer =
-    (glob_constr_and_expr -> std_ppcmds) ->
-    (glob_constr_and_expr -> std_ppcmds) ->
-    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-    'a -> std_ppcmds
+  type 'a raw_extra_genarg_printer =
+      (constr_expr -> std_ppcmds) ->
+      (constr_expr -> std_ppcmds) ->
+      (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+      'a -> std_ppcmds
 
-type 'a extra_genarg_printer =
-    (Term.constr -> std_ppcmds) ->
-    (Term.constr -> std_ppcmds) ->
-    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-    'a -> std_ppcmds
+  type 'a glob_extra_genarg_printer =
+      (glob_constr_and_expr -> std_ppcmds) ->
+      (glob_constr_and_expr -> std_ppcmds) ->
+      (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+      'a -> std_ppcmds
 
-let genarg_pprule = ref String.Map.empty
+  type 'a extra_genarg_printer =
+      (Term.constr -> std_ppcmds) ->
+      (Term.constr -> std_ppcmds) ->
+      (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+      'a -> std_ppcmds
 
-let declare_extra_genarg_pprule wit f g h =
-  let s = match unquote (topwit wit) with
-    | ExtraArgType s -> 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
+  let genarg_pprule = ref String.Map.empty
 
-let pr_arg pr x = spc () ++ pr x
+  let declare_extra_genarg_pprule wit f g h =
+    let s = match unquote (topwit wit) with
+      | ExtraArgType s -> 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
+
+  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_or_var pr = function
+    | ArgArg x -> pr x
+    | ArgVar (_,s) -> pr_id s
 
-let pr_and_short_name pr (c,_) = pr c
+  let pr_and_short_name pr (c,_) = pr c
 
-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 pr_or_by_notation f = function
+    | AN v -> f v
+    | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
-let pr_located pr (loc,x) = pr x
+  let pr_located pr (loc,x) = pr x
 
-let pr_evaluable_reference = function
-  | EvalVarRef id -> pr_id id
-  | EvalConstRef sp -> pr_global (Globnames.ConstRef sp)
+  let pr_evaluable_reference = function
+    | EvalVarRef id -> pr_id id
+    | EvalConstRef sp -> pr_global (Globnames.ConstRef sp)
 
-let pr_quantified_hypothesis = function
-  | AnonHyp n -> int n
-  | NamedHyp id -> pr_id id
+  let pr_quantified_hypothesis = function
+    | AnonHyp n -> int n
+    | NamedHyp id -> pr_id id
 
-let pr_binding prc = function
-  | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
-  | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+  let pr_binding prc = function
+    | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
+    | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
 
-let pr_bindings prc prlc = function
-  | ImplicitBindings l ->
+  let pr_bindings prc prlc = function
+    | ImplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
-      hv 0 (prlist_with_sep spc prc l)
-  | ExplicitBindings l ->
+        hv 0 (prlist_with_sep spc prc l)
+    | ExplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
         hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l)
-  | NoBindings -> mt ()
+    | NoBindings -> mt ()
 
-let pr_bindings_no_with prc prlc = function
-  | ImplicitBindings l ->
+  let pr_bindings_no_with prc prlc = function
+    | ImplicitBindings l ->
       brk (0,1) ++
-      prlist_with_sep spc prc l
-  | ExplicitBindings l ->
+        prlist_with_sep spc prc l
+    | ExplicitBindings l ->
       brk (0,1) ++
         prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
-  | NoBindings -> mt ()
-
-let pr_clear_flag clear_flag pp x =
-  (match clear_flag with Some false -> str "!" | Some true -> str ">" | None -> mt())
-  ++ pp x
-
-let pr_with_bindings prc prlc (c,bl) =
-  prc c ++ pr_bindings prc prlc bl
-
-let pr_with_bindings_arg prc prlc (clear_flag,c) =
-  pr_clear_flag clear_flag (pr_with_bindings prc prlc) c
-
-let pr_with_constr prc = function
-  | None -> mt ()
-  | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
-
-let pr_message_token prid = function
-  | MsgString s -> qs s
-  | MsgInt n -> int n
-  | MsgIdent id -> prid id
-
-let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s)
-
-let with_evars ev s = if ev then "e" ^ s else s
-
-
-let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
-  match Genarg.genarg_tag x with
-  | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
-  | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
-  | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
-  | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
-  | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
-  | ConstrMayEvalArgType ->
-      pr_may_eval prc prlc (pr_or_by_notation prref) prpat
-        (out_gen (rawwit wit_constr_may_eval) x)
-  | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x)
-  | RedExprArgType ->
-      pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
-        (out_gen (rawwit wit_red_expr) x)
-  | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
-  | ConstrWithBindingsArgType ->
-      pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x)
-  | BindingsArgType ->
-      pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x)
-  | ListArgType _ ->
-      let list_unpacker wit l =
-        let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
-        pr_sequence map (raw l)
-      in
-      hov 0 (list_unpack { list_unpacker } x)
-  | OptArgType _ ->
-      let opt_unpacker wit o = match raw o with
-      | None -> mt ()
-      | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x)
-      in
-      hov 0 (opt_unpack { opt_unpacker } x)
-  | PairArgType _ ->
-      let pair_unpacker wit1 wit2 o =
-        let p, q = raw o in
-        let p = in_gen (rawwit wit1) p in
-        let q = in_gen (rawwit wit2) q in
-        pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q]
-      in
-      hov 0 (pair_unpack { pair_unpacker } x)
-  | ExtraArgType s ->
-      try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x
-      with Not_found -> Genprint.generic_raw_print x
-
-
-let rec pr_glb_generic prc prlc prtac prpat x =
-  match Genarg.genarg_tag x with
-  | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
-  | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
-  | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
-  | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
-  | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
-  | ConstrMayEvalArgType ->
-      pr_may_eval prc prlc
-        (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat
-        (out_gen (glbwit wit_constr_may_eval) x)
-  | QuantHypArgType ->
-      pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x)
-  | RedExprArgType ->
-      pr_red_expr
-        (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
-        (out_gen (glbwit wit_red_expr) x)
-  | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
-  | ConstrWithBindingsArgType ->
-      pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x)
-  | BindingsArgType ->
-      pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x)
-  | ListArgType _ ->
-      let list_unpacker wit l =
-        let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in
-        pr_sequence map (glb l)
-      in
-      hov 0 (list_unpack { list_unpacker } x)
-  | OptArgType _ ->
-      let opt_unpacker wit o = match glb o with
-      | None -> mt ()
-      | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x)
-      in
-      hov 0 (opt_unpack { opt_unpacker } x)
-  | PairArgType _ ->
-      let pair_unpacker wit1 wit2 o =
-        let p, q = glb o in
-        let p = in_gen (glbwit wit1) p in
-        let q = in_gen (glbwit wit2) q in
-        pr_sequence (pr_glb_generic prc prlc prtac prpat) [p; q]
-      in
-      hov 0 (pair_unpack { pair_unpacker } x)
-  | ExtraArgType s ->
-      try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x
-      with Not_found -> Genprint.generic_glb_print x
-
-let rec pr_top_generic prc prlc prtac prpat x =
-  match Genarg.genarg_tag x with
-  | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
-  | IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
-  | VarArgType -> pr_id (out_gen (topwit wit_var) x)
-  | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
-  | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
-  | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
-  | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x)
-  | RedExprArgType ->
-      pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
-        (out_gen (topwit wit_red_expr) x)
-  | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
-  | ConstrWithBindingsArgType ->
-      let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in
-      pr_with_bindings prc prlc (c,b)
-  | BindingsArgType ->
-      pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it
-  | ListArgType _ ->
-      let list_unpacker wit l =
-        let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in
-        pr_sequence map (top l)
-      in
-      hov 0 (list_unpack { list_unpacker } x)
-  | OptArgType _ ->
-      let opt_unpacker wit o = match top o with
-      | None -> mt ()
-      | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x)
-      in
-      hov 0 (opt_unpack { opt_unpacker } x)
-  | PairArgType _ ->
-      let pair_unpacker wit1 wit2 o =
-        let p, q = top o in
-        let p = in_gen (topwit wit1) p in
-        let q = in_gen (topwit wit2) q in
-        pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q]
-      in
-      hov 0 (pair_unpack { pair_unpacker } x)
-  | ExtraArgType s ->
-      try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x
-      with Not_found -> Genprint.generic_top_print x
-
-let rec tacarg_using_rule_token pr_gen = function
-  | Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al)
-  | None :: l, a :: al ->
+    | NoBindings -> mt ()
+
+  let pr_clear_flag clear_flag pp x =
+    (match clear_flag with Some false -> str "!" | Some true -> str ">" | None -> mt())
+    ++ pp x
+
+  let pr_with_bindings prc prlc (c,bl) =
+    prc c ++ pr_bindings prc prlc bl
+
+  let pr_with_bindings_arg prc prlc (clear_flag,c) =
+    pr_clear_flag clear_flag (pr_with_bindings prc prlc) c
+
+  let pr_with_constr prc = function
+    | None -> mt ()
+    | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
+
+  let pr_message_token prid = function
+    | MsgString s -> qs s
+    | MsgInt n -> int n
+    | MsgIdent id -> prid id
+
+  let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s)
+
+  let with_evars ev s = if ev then "e" ^ s else s
+
+
+  let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
+    match Genarg.genarg_tag x with
+      | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
+      | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
+      | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
+      | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
+      | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
+      | ConstrMayEvalArgType ->
+        pr_may_eval prc prlc (pr_or_by_notation prref) prpat
+          (out_gen (rawwit wit_constr_may_eval) x)
+      | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x)
+      | RedExprArgType ->
+        pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
+          (out_gen (rawwit wit_red_expr) x)
+      | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
+      | ConstrWithBindingsArgType ->
+        pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x)
+      | BindingsArgType ->
+        pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x)
+      | ListArgType _ ->
+        let list_unpacker wit l =
+          let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
+          pr_sequence map (raw l)
+        in
+        hov 0 (list_unpack { list_unpacker } x)
+      | OptArgType _ ->
+        let opt_unpacker wit o = match raw o with
+          | None -> mt ()
+          | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x)
+        in
+        hov 0 (opt_unpack { opt_unpacker } x)
+      | PairArgType _ ->
+        let pair_unpacker wit1 wit2 o =
+          let p, q = raw o in
+          let p = in_gen (rawwit wit1) p in
+          let q = in_gen (rawwit wit2) q in
+          pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q]
+        in
+        hov 0 (pair_unpack { pair_unpacker } x)
+      | ExtraArgType s ->
+        try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x
+        with Not_found -> Genprint.generic_raw_print x
+
+
+  let rec pr_glb_generic prc prlc prtac prpat x =
+    match Genarg.genarg_tag x with
+      | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
+      | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
+      | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
+      | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
+      | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
+      | ConstrMayEvalArgType ->
+        pr_may_eval prc prlc
+          (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat
+          (out_gen (glbwit wit_constr_may_eval) x)
+      | QuantHypArgType ->
+        pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x)
+      | RedExprArgType ->
+        pr_red_expr
+          (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
+          (out_gen (glbwit wit_red_expr) x)
+      | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
+      | ConstrWithBindingsArgType ->
+        pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x)
+      | BindingsArgType ->
+        pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x)
+      | ListArgType _ ->
+        let list_unpacker wit l =
+          let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in
+          pr_sequence map (glb l)
+        in
+        hov 0 (list_unpack { list_unpacker } x)
+      | OptArgType _ ->
+        let opt_unpacker wit o = match glb o with
+          | None -> mt ()
+          | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x)
+        in
+        hov 0 (opt_unpack { opt_unpacker } x)
+      | PairArgType _ ->
+        let pair_unpacker wit1 wit2 o =
+          let p, q = glb o in
+          let p = in_gen (glbwit wit1) p in
+          let q = in_gen (glbwit wit2) q in
+          pr_sequence (pr_glb_generic prc prlc prtac prpat) [p; q]
+        in
+        hov 0 (pair_unpack { pair_unpacker } x)
+      | ExtraArgType s ->
+        try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x
+        with Not_found -> Genprint.generic_glb_print x
+
+  let rec pr_top_generic prc prlc prtac prpat x =
+    match Genarg.genarg_tag x with
+      | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
+      | IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
+      | VarArgType -> pr_id (out_gen (topwit wit_var) x)
+      | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
+      | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
+      | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
+      | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x)
+      | RedExprArgType ->
+        pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
+          (out_gen (topwit wit_red_expr) x)
+      | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
+      | ConstrWithBindingsArgType ->
+        let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in
+        pr_with_bindings prc prlc (c,b)
+      | BindingsArgType ->
+        pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it
+      | ListArgType _ ->
+        let list_unpacker wit l =
+          let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in
+          pr_sequence map (top l)
+        in
+        hov 0 (list_unpack { list_unpacker } x)
+      | OptArgType _ ->
+        let opt_unpacker wit o = match top o with
+          | None -> mt ()
+          | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x)
+        in
+        hov 0 (opt_unpack { opt_unpacker } x)
+      | PairArgType _ ->
+        let pair_unpacker wit1 wit2 o =
+          let p, q = top o in
+          let p = in_gen (topwit wit1) p in
+          let q = in_gen (topwit wit2) q in
+          pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q]
+        in
+        hov 0 (pair_unpack { pair_unpacker } x)
+      | ExtraArgType s ->
+        try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x
+        with Not_found -> Genprint.generic_top_print x
+
+  let rec tacarg_using_rule_token pr_gen = function
+    | Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al)
+    | None :: l, a :: al ->
       let r = tacarg_using_rule_token pr_gen (l,al) in
       pr_gen a :: r
-  | [], [] -> []
-  | _ -> failwith "Inconsistent arguments of extended tactic"
-
-let pr_tacarg_using_rule pr_gen l=
-  pr_sequence (fun x -> x) (tacarg_using_rule_token pr_gen l)
-
-let pr_extend_gen pr_gen lev s l =
-  try
-    let tags = List.map genarg_tag l in
-    let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
-    let p = pr_tacarg_using_rule pr_gen (pl,l) in
-    if lev' > lev then surround p else p
-  with Not_found ->
-    let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in
-    let args = match l with
-    | [] -> mt ()
-    | _ -> spc() ++ pr_sequence pr_gen l
-    in
-    str "<" ++ name ++ str ">" ++ args
-
-let pr_alias_gen pr_gen lev key l =
-  try
-    let pp = KNmap.find key !prnotation_tab in
-    let (lev', pl) = pp.pptac_prods in
-    let p = pr_tacarg_using_rule pr_gen (pl, l) in
-    if lev' > lev then surround p else p
-  with Not_found ->
-    KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
-
-let pr_raw_extend prc prlc prtac prpat =
-  pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
-let pr_glob_extend prc prlc prtac prpat =
-  pr_extend_gen (pr_glb_generic prc prlc prtac prpat)
-let pr_extend prc prlc prtac prpat =
-  pr_extend_gen (pr_top_generic prc prlc prtac prpat)
-
-let pr_raw_alias prc prlc prtac prpat =
-  pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
-let pr_glob_alias prc prlc prtac prpat =
-  pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
-let pr_alias prc prlc prtac prpat =
-  pr_alias_gen (pr_top_generic prc prlc prtac prpat)
-
-(**********************************************************************)
-(* The tactic printer                                                 *)
-
-let strip_prod_binders_expr n ty =
-  let rec strip_ty acc n ty =
-    match ty with
-        Constrexpr.CProdN(_,bll,a) ->
-          let nb =
-            List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
-	  let bll = List.map (fun (x, _, y) -> x, y) bll in
+    | [], [] -> []
+    | _ -> failwith "Inconsistent arguments of extended tactic"
+
+  let pr_tacarg_using_rule pr_gen l=
+    pr_sequence (fun x -> x) (tacarg_using_rule_token pr_gen l)
+
+  let pr_extend_gen pr_gen lev s l =
+    try
+      let tags = List.map genarg_tag l in
+      let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
+      let p = pr_tacarg_using_rule pr_gen (pl,l) in
+      if lev' > lev then surround p else p
+    with Not_found ->
+      let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in
+      let args = match l with
+        | [] -> mt ()
+        | _ -> spc() ++ pr_sequence pr_gen l
+      in
+      str "<" ++ name ++ str ">" ++ args
+
+  let pr_alias_gen pr_gen lev key l =
+    try
+      let pp = KNmap.find key !prnotation_tab in
+      let (lev', pl) = pp.pptac_prods in
+      let p = pr_tacarg_using_rule pr_gen (pl, l) in
+      if lev' > lev then surround p else p
+    with Not_found ->
+      KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
+
+  let pr_raw_extend prc prlc prtac prpat =
+    pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
+  let pr_glob_extend prc prlc prtac prpat =
+    pr_extend_gen (pr_glb_generic prc prlc prtac prpat)
+  let pr_extend prc prlc prtac prpat =
+    pr_extend_gen (pr_top_generic prc prlc prtac prpat)
+
+  let pr_raw_alias prc prlc prtac prpat =
+    pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
+  let pr_glob_alias prc prlc prtac prpat =
+    pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
+  let pr_alias prc prlc prtac prpat =
+    pr_alias_gen (pr_top_generic prc prlc prtac prpat)
+
+  (**********************************************************************)
+  (* The tactic printer                                                 *)
+
+  let strip_prod_binders_expr n ty =
+    let rec strip_ty acc n ty =
+      match ty with
+          Constrexpr.CProdN(_,bll,a) ->
+            let nb =
+              List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
+            let bll = List.map (fun (x, _, y) -> x, y) bll in
             if nb >= n then (List.rev (bll@acc)), a
             else strip_ty (bll@acc) (n-nb) a
-      | _ -> error "Cannot translate fix tactic: not enough products" in
-  strip_ty [] n ty
-
-let pr_ltac_or_var pr = function
-  | ArgArg x -> pr x
-  | ArgVar (loc,id) -> pr_with_comments loc (pr_id id)
-
-let pr_ltac_constant kn =
-  if !Flags.in_debugger then pr_kn kn
-  else try
-    pr_qualid (Nametab.shortest_qualid_of_tactic kn)
-  with Not_found -> (* local tactic not accessible anymore *)
-    str "<" ++ pr_kn kn ++ str ">"
-
-let pr_evaluable_reference_env env = function
-  | EvalVarRef id -> pr_id id
-  | EvalConstRef sp ->
+        | _ -> error "Cannot translate fix tactic: not enough products" in
+    strip_ty [] n ty
+
+  let pr_ltac_or_var pr = function
+    | ArgArg x -> pr x
+    | ArgVar (loc,id) -> pr_with_comments loc (pr_id id)
+
+  let pr_ltac_constant kn =
+    if !Flags.in_debugger then pr_kn kn
+    else try
+           pr_qualid (Nametab.shortest_qualid_of_tactic kn)
+      with Not_found -> (* local tactic not accessible anymore *)
+        str "<" ++ pr_kn kn ++ str ">"
+
+  let pr_evaluable_reference_env env = function
+    | EvalVarRef id -> pr_id id
+    | EvalConstRef sp ->
       Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp)
 
-let pr_esubst prc l =
-  let pr_qhyp = function
-      (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
-    | (_,NamedHyp id,c) ->
+  let pr_esubst prc l =
+    let pr_qhyp = function
+    (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
+      | (_,NamedHyp id,c) ->
         str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
-  in
-  prlist_with_sep spc pr_qhyp l
+    in
+    prlist_with_sep spc pr_qhyp l
 
-let pr_bindings_gen for_ex prc prlc = function
-  | ImplicitBindings l ->
+  let pr_bindings_gen for_ex prc prlc = function
+    | ImplicitBindings l ->
       spc () ++
-      hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++
-            prlist_with_sep spc prc l)
-  | ExplicitBindings l ->
+        hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++
+                 prlist_with_sep spc prc l)
+    | ExplicitBindings l ->
       spc () ++
-      hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++
-            pr_esubst prlc l)
-  | NoBindings -> mt ()
+        hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++
+                 pr_esubst prlc l)
+    | NoBindings -> mt ()
 
-let pr_bindings prc prlc = pr_bindings_gen false prc prlc
+  let pr_bindings prc prlc = pr_bindings_gen false prc prlc
 
-let pr_with_bindings prc prlc (c,bl) =
-  hov 1 (prc c ++ pr_bindings prc prlc bl)
+  let pr_with_bindings prc prlc (c,bl) =
+    hov 1 (prc c ++ pr_bindings prc prlc bl)
 
-let pr_as_disjunctive_ipat prc ipatl =
-  str "as " ++
-  pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
+  let pr_as_disjunctive_ipat prc ipatl =
+    str "as " ++
+      pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
 
-let pr_eqn_ipat (_,ipat) = str "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
+  let pr_eqn_ipat (_,ipat) = str "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
 
-let pr_with_induction_names prc = function
-  | None, None -> mt ()
-  | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat)
-  | None, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat prc ipat)
-  | Some eqpat, Some ipat ->
+  let pr_with_induction_names prc = function
+    | None, None -> mt ()
+    | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat)
+    | None, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat prc ipat)
+    | Some eqpat, Some ipat ->
       spc () ++
-      hov 1 (pr_as_disjunctive_ipat prc ipat ++ spc () ++ pr_eqn_ipat eqpat)
+        hov 1 (pr_as_disjunctive_ipat prc ipat ++ spc () ++ pr_eqn_ipat eqpat)
 
-let pr_as_intro_pattern prc ipat =
-  spc () ++ hov 1 (str "as" ++ spc () ++ Miscprint.pr_intro_pattern prc ipat)
+  let pr_as_intro_pattern prc ipat =
+    spc () ++ hov 1 (str "as" ++ spc () ++ Miscprint.pr_intro_pattern prc ipat)
 
-let pr_with_inversion_names prc = function
-  | None -> mt ()
-  | Some ipat -> pr_as_disjunctive_ipat prc ipat
+  let pr_with_inversion_names prc = function
+    | None -> mt ()
+    | Some ipat -> pr_as_disjunctive_ipat prc ipat
 
-let pr_as_ipat prc = function
-  | None -> mt ()
-  | Some ipat -> pr_as_intro_pattern prc ipat
+  let pr_as_ipat prc = function
+    | None -> mt ()
+    | Some ipat -> pr_as_intro_pattern prc ipat
 
-let pr_as_name = function
-  | Anonymous -> mt ()
-  | Name id -> str " as " ++ pr_lident (Loc.ghost,id)
+  let pr_as_name = function
+    | Anonymous -> mt ()
+    | Name id -> str " as " ++ pr_lident (Loc.ghost,id)
 
-let pr_pose_as_style prc na c =
-  spc() ++ prc c ++ pr_as_name na
+  let pr_pose_as_style prc na c =
+    spc() ++ prc c ++ pr_as_name na
 
-let pr_pose prc prlc na c = match na with
-  | Anonymous -> spc() ++ prc c
-  | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c)
+  let pr_pose prc prlc na c = match na with
+    | Anonymous -> spc() ++ prc c
+    | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c)
 
-let pr_assertion prc prdc _prlc ipat c = match ipat with
-(* Use this "optimisation" or use only the general case ?
-  | IntroIdentifier id ->
-      spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
-*)
-  | ipat ->
+  let pr_assertion prc prdc _prlc ipat c = match ipat with
+    (* Use this "optimisation" or use only the general case ?
+       | IntroIdentifier id ->
+       spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
+    *)
+    | ipat ->
       spc() ++ prc c ++ pr_as_ipat prdc ipat
 
-let pr_assumption prc prdc prlc ipat c = match ipat with
-(* Use this "optimisation" or use only the general case ?*)
-(* it seems that this "optimisation" is somehow more natural *)
-  | Some (_,IntroNaming (IntroIdentifier id)) ->
+  let pr_assumption prc prdc prlc ipat c = match ipat with
+    (* Use this "optimisation" or use only the general case ?*)
+    (* it seems that this "optimisation" is somehow more natural *)
+    | Some (_,IntroNaming (IntroIdentifier id)) ->
       spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c)
-  | ipat ->
+    | ipat ->
       spc() ++ prc c ++ pr_as_ipat prdc ipat
 
-let pr_by_tactic prt = function
-  | TacId [] -> mt ()
-  | tac -> spc() ++ str "by " ++ prt tac
+  let pr_by_tactic prt = function
+    | TacId [] -> mt ()
+    | tac -> spc() ++ str "by " ++ prt tac
 
-let pr_hyp_location pr_id = function
-  | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
-  | occs, InHypTypeOnly ->
+  let pr_hyp_location pr_id = function
+    | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
+    | occs, InHypTypeOnly ->
       spc () ++
-      pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs
-  | occs, InHypValueOnly ->
+        pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs
+    | occs, InHypValueOnly ->
       spc () ++
-      pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs
+        pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs
 
-let pr_in pp = spc () ++ hov 0 (str "in" ++ pp)
+  let pr_in pp = spc () ++ hov 0 (str "in" ++ pp)
 
-let pr_simple_hyp_clause pr_id = function
-  | [] -> mt ()
-  | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
+  let pr_simple_hyp_clause pr_id = function
+    | [] -> mt ()
+    | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
 
-let pr_in_hyp_as prc pr_id = function
-  | None -> mt ()
-  | Some (clear,id,ipat) ->
+  let pr_in_hyp_as prc pr_id = function
+    | None -> mt ()
+    | Some (clear,id,ipat) ->
       pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat prc ipat
 
-let pr_clauses default_is_concl pr_id = function
-  | { onhyps=Some []; concl_occs=occs }
-      when (match default_is_concl with Some true -> true | _ -> false) ->
+  let pr_clauses default_is_concl pr_id = function
+    | { onhyps=Some []; concl_occs=occs }
+        when (match default_is_concl with Some true -> true | _ -> false) ->
       pr_with_occurrences mt (occs,())
-  | { onhyps=None; concl_occs=AllOccurrences }
-      when (match default_is_concl with Some false -> true | _ -> false) -> mt ()
-  | { onhyps=None; concl_occs=NoOccurrences } ->
+    | { onhyps=None; concl_occs=AllOccurrences }
+        when (match default_is_concl with Some false -> true | _ -> false) -> mt ()
+    | { onhyps=None; concl_occs=NoOccurrences } ->
       pr_in (str " * |-")
-  | { onhyps=None; concl_occs=occs } ->
+    | { onhyps=None; concl_occs=occs } ->
       pr_in (pr_with_occurrences (fun () -> str " *") (occs,()))
-  | { onhyps=Some l; concl_occs=occs } ->
+    | { onhyps=Some l; concl_occs=occs } ->
       let pr_occs = match occs with
-      | NoOccurrences -> mt ()
-      | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,())
+        | NoOccurrences -> mt ()
+        | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,())
       in
       pr_in
         (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++ pr_occs)
 
-let pr_orient b = if b then mt () else str "<- "
+  let pr_orient b = if b then mt () else str "<- "
 
-let pr_multi = function
-  | Precisely 1 -> mt ()
-  | Precisely n -> int n ++ str "!"
-  | UpTo n -> int n ++ str "?"
-  | RepeatStar -> str "?"
-  | RepeatPlus -> str "!"
+  let pr_multi = function
+    | Precisely 1 -> mt ()
+    | Precisely n -> int n ++ str "!"
+    | UpTo n -> int n ++ str "?"
+    | RepeatStar -> str "?"
+    | RepeatPlus -> str "!"
 
-let pr_induction_arg prc prlc = function
-  | ElimOnConstr c -> pr_with_bindings prc prlc c
-  | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
-  | ElimOnAnonHyp n -> int n
+  let pr_induction_arg prc prlc = function
+    | ElimOnConstr c -> pr_with_bindings prc prlc c
+    | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
+    | ElimOnAnonHyp n -> int n
 
-let pr_induction_kind = function
-  | SimpleInversion -> str "simple inversion"
-  | FullInversion -> str "inversion"
-  | FullInversionClear -> str "inversion_clear"
+  let pr_induction_kind = function
+    | SimpleInversion -> str "simple inversion"
+    | FullInversion -> str "inversion"
+    | FullInversionClear -> str "inversion_clear"
 
-let pr_lazy lz = if lz then str "lazy" else mt ()
+  let pr_lazy lz = if lz then str "lazy" else mt ()
 
-let pr_match_pattern pr_pat = function
-  | Term a -> pr_pat a
-  | Subterm (b,None,a) ->
+  let pr_match_pattern pr_pat = function
+    | Term a -> pr_pat a
+    | Subterm (b,None,a) ->
     (** ppedrot: we don't make difference between [appcontext] and [context]
         anymore, and the interpretation is governed by a flag instead. *)
-    str "context [" ++ pr_pat a ++ str "]"
-  | Subterm (b,Some id,a) ->
-    str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+      str "context [" ++ pr_pat a ++ str "]"
+    | Subterm (b,Some id,a) ->
+      str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
 
-let pr_match_hyps pr_pat = function
-  | Hyp (nal,mp) ->
+  let pr_match_hyps pr_pat = function
+    | Hyp (nal,mp) ->
       pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
-  | Def (nal,mv,mp) ->
+    | Def (nal,mv,mp) ->
       pr_lname nal ++ str ":=" ++ pr_match_pattern pr_pat mv
       ++ str ":" ++ pr_match_pattern pr_pat mp
 
-let pr_match_rule m pr pr_pat = function
-  | Pat ([],mp,t) when m ->
+  let pr_match_rule m pr pr_pat = function
+    | Pat ([],mp,t) when m ->
       pr_match_pattern pr_pat mp ++
-      spc () ++ str "=>" ++ brk (1,4) ++ pr t
-(*
-  | Pat (rl,mp,t) ->
+        spc () ++ str "=>" ++ brk (1,4) ++ pr t
+    (*
+      | Pat (rl,mp,t) ->
       hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl ++
-        (if rl <> [] then spc () else mt ()) ++
-         hov 0 (str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
-	 str "=>" ++ brk (1,4) ++ pr t))
-*)
-  | Pat (rl,mp,t) ->
+      (if rl <> [] then spc () else mt ()) ++
+      hov 0 (str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+      str "=>" ++ brk (1,4) ++ pr t))
+    *)
+    | Pat (rl,mp,t) ->
       hov 0 (
-	hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl) ++
-        (if not (List.is_empty rl) then spc () else mt ()) ++
-        hov 0 (
-	  str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
-	  str "=>" ++ brk (1,4) ++ pr t))
-  | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
-
-let pr_funvar = function
-  | None -> spc () ++ str "_"
-  | Some id -> spc () ++ pr_id id
-
-let pr_let_clause k pr (id,(bl,t)) =
-  hov 0 (str k ++ pr_lident id ++ prlist pr_funvar bl ++
-         str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.ghost,t)))
-
-let pr_let_clauses recflag pr = function
-  | hd::tl ->
+        hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl) ++
+          (if not (List.is_empty rl) then spc () else mt ()) ++
+          hov 0 (
+            str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+              str "=>" ++ brk (1,4) ++ pr t))
+    | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
+
+  let pr_funvar = function
+    | None -> spc () ++ str "_"
+    | Some id -> spc () ++ pr_id id
+
+  let pr_let_clause k pr (id,(bl,t)) =
+    hov 0 (str k ++ pr_lident id ++ prlist pr_funvar bl ++
+             str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.ghost,t)))
+
+  let pr_let_clauses recflag pr = function
+    | hd::tl ->
       hv 0
         (pr_let_clause (if recflag then "let rec " else "let ") pr hd ++
-         prlist (fun t -> spc () ++ pr_let_clause "with " pr t) tl)
-  | [] -> anomaly (Pp.str "LetIn must declare at least one binding")
-
-let pr_seq_body pr tl =
-  hv 0 (str "[ " ++
-        prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
-        str " ]")
-
-let pr_dispatch pr tl =
-  hv 0 (str "[>" ++
-        prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
-        str " ]")
-
-let pr_opt_tactic pr = function
-  | TacId [] -> mt ()
-  | t -> pr t
-
-let pr_tac_extend_gen pr tf tm tl =
-  prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++
-  pr_opt_tactic pr tm ++ str ".." ++
-  prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl
-
-let pr_then_gen pr tf tm tl =
-  hv 0 (str "[ " ++
-        pr_tac_extend_gen pr tf tm tl ++
-        str " ]")
-
-let pr_tac_extend pr tf tm tl =
-  hv 0 (str "[>" ++
-        pr_tac_extend_gen pr tf tm tl ++
-        str " ]")
-
-let pr_hintbases = function
-  | None -> spc () ++ str "with *"
-  | Some [] -> mt ()
-  | Some l ->
+           prlist (fun t -> spc () ++ pr_let_clause "with " pr t) tl)
+    | [] -> anomaly (Pp.str "LetIn must declare at least one binding")
+
+  let pr_seq_body pr tl =
+    hv 0 (str "[ " ++
+            prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
+            str " ]")
+
+  let pr_dispatch pr tl =
+    hv 0 (str "[>" ++
+            prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
+            str " ]")
+
+  let pr_opt_tactic pr = function
+    | TacId [] -> mt ()
+    | t -> pr t
+
+  let pr_tac_extend_gen pr tf tm tl =
+    prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++
+      pr_opt_tactic pr tm ++ str ".." ++
+      prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl
+
+  let pr_then_gen pr tf tm tl =
+    hv 0 (str "[ " ++
+            pr_tac_extend_gen pr tf tm tl ++
+            str " ]")
+
+  let pr_tac_extend pr tf tm tl =
+    hv 0 (str "[>" ++
+            pr_tac_extend_gen pr tf tm tl ++
+            str " ]")
+
+  let pr_hintbases = function
+    | None -> spc () ++ str "with *"
+    | Some [] -> mt ()
+    | Some l ->
       spc () ++ hov 2 (str "with" ++ prlist (fun s -> spc () ++ str s) l)
 
-let pr_auto_using prc = function
-  | [] -> mt ()
-  | l -> spc () ++
+  let pr_auto_using prc = function
+    | [] -> mt ()
+    | l -> spc () ++
       hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
 
-let string_of_debug = function
-  | Off -> ""
-  | Debug -> "debug "
-  | Info -> "info_"
-
-let pr_then () = str ";"
-
-let ltop = (5,E)
-let lseq = 4
-let ltactical = 3
-let lorelse = 2
-let llet = 5
-let lfun = 5
-let lcomplete = 1
-let labstract = 3
-let lmatch = 1
-let latom = 0
-let lcall = 1
-let leval = 1
-let ltatom = 1
-let linfo = 5
-
-let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
+  let string_of_debug = function
+    | Off -> ""
+    | Debug -> "debug "
+    | Info -> "info_"
+
+  let pr_then () = str ";"
+
+  let ltop = (5,E)
+  let lseq = 4
+  let ltactical = 3
+  let lorelse = 2
+  let llet = 5
+  let lfun = 5
+  let lcomplete = 1
+  let labstract = 3
+  let lmatch = 1
+  let latom = 0
+  let lcall = 1
+  let leval = 1
+  let ltatom = 1
+  let linfo = 5
+
+  let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
 
 (** A printer for tactics that polymorphically works on the three
     "raw", "glob" and "typed" levels *)
 
-type 'a printer = {
-  pr_tactic : tolerability -> 'tacexpr -> std_ppcmds;
-  pr_constr : 'trm -> std_ppcmds;
-  pr_uconstr: 'utrm -> std_ppcmds;
-  pr_lconstr : 'trm -> std_ppcmds;
-  pr_dconstr: 'dtrm -> std_ppcmds;
-  pr_pattern : 'pat -> std_ppcmds;
-  pr_lpattern : 'pat -> std_ppcmds;
-  pr_constant : 'cst -> std_ppcmds;
-  pr_reference : 'ref -> std_ppcmds;
-  pr_name : 'nam -> std_ppcmds;
-  pr_generic : 'lev generic_argument -> std_ppcmds;
-  pr_extend : int -> ml_tactic_name -> 'lev generic_argument list -> std_ppcmds;
-  pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds;
-}
-
-constraint 'a = <
-    term:'trm;
-    utrm:'utrm;
-    dterm:'dtrm;
-    pattern:'pat;
-    constant:'cst;
-    reference:'ref;
-    name:'nam;
-    tacexpr:'tacexpr;
-    level:'lev
->
-
-let make_pr_tac pr
-  (strip_prod_binders) =
-
-(* some shortcuts *)
-let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in
-let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in
-let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
-let pr_with_bindings_arg_full = pr_with_bindings_arg in
-let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
-let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
-
-let pr_constrarg c = spc () ++ pr.pr_constr c in
-let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
-let pr_intarg n = spc () ++ int n in
-
-(* Some printing combinators *)
-let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in
-
-let extract_binders = function
-  | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
-  | body -> ([],body) in
-
-let pr_binder_fix (nal,t) =
-(*  match t with
-  | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
-  | _ ->*)
-    let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
-    spc() ++ hov 1 (str"(" ++ s ++ str")") in
-
-let pr_fix_tac (id,n,c) =
-  let rec set_nth_name avoid n = function
-      (nal,ty)::bll ->
-        if n <= List.length nal then
-          match List.chop (n-1) nal with
-              _, (_,Name id) :: _ -> id, (nal,ty)::bll
-            | bef, (loc,Anonymous) :: aft ->
-                let id = next_ident_away (Id.of_string"y") avoid in
-                id, ((bef@(loc,Name id)::aft, ty)::bll)
-            | _ -> assert false
-        else
-          let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
-          (id,(nal,ty)::bll')
-    | [] -> assert false in
-  let (bll,ty) = strip_prod_binders n c in
-  let names =
-    List.fold_left
-      (fun ln (nal,_) -> List.fold_left
-          (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
-          ln nal)
-      [] bll in
-  let idarg,bll = set_nth_name names n bll in
-  let annot = match names with
-  | [_] -> mt ()
-  | _ -> spc() ++ str"{struct " ++ pr_id idarg ++ str"}"
-  in
-  hov 1 (str"(" ++ pr_id id ++
-        prlist pr_binder_fix bll ++ annot ++ str" :" ++
-        pr_lconstrarg ty ++ str")") in
-(*  spc() ++
-  hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
-    c)
-*)
-let pr_cofix_tac (id,c) =
-  hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
-
-  (* Printing tactics as arguments *)
-let rec pr_atom0 = function
-  | TacIntroPattern [] -> str "intros"
-  | TacIntroMove (None,MoveLast) -> str "intro"
-  | TacTrivial (d,[],Some []) -> str (string_of_debug d ^ "trivial")
-  | TacAuto (d,None,[],Some []) -> str (string_of_debug d ^ "auto")
-  | TacClear (true,[]) -> str "clear"
-  | t -> str "(" ++ pr_atom1 t ++ str ")"
-
-  (* Main tactic printer *)
-and pr_atom1 = function
-  (* Basic tactics *)
-  | TacIntroPattern [] as t -> pr_atom0 t
-  | TacIntroPattern (_::_ as p) ->
-      hov 1 (str "intros" ++ spc () ++
-             prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
-  | 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 ++
-             Miscprint.pr_move_location pr.pr_name hto)
-  | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
-  | TacApply (a,ev,cb,inhyp) ->
-      hov 1 ((if a then mt() else str "simple ") ++
-             str (with_evars ev "apply") ++ spc () ++
-             prlist_with_sep pr_comma pr_with_bindings_arg cb ++
-             pr_in_hyp_as pr.pr_dconstr pr.pr_name inhyp)
-  | TacElim (ev,cb,cbo) ->
-      hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings_arg cb ++
-        pr_opt pr_eliminator cbo)
-  | TacCase (ev,cb) ->
-      hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
-  | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
-  | TacMutualFix (id,n,l) ->
-      hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
-             str"with " ++ prlist_with_sep spc pr_fix_tac l)
-  | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
-  | TacMutualCofix (id,l) ->
-      hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
-             str"with " ++ prlist_with_sep spc pr_cofix_tac l)
-  | TacAssert (b,Some tac,ipat,c) ->
-      hov 1 (str (if b then "assert" else "enough") ++
-             pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
-             pr_by_tactic (pr.pr_tactic ltop) tac)
-  | TacAssert (_,None,ipat,c) ->
-      hov 1 (str "pose proof" ++
-             pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c)
-  | TacGeneralize l ->
-      hov 1 (str "generalize" ++ spc () ++
-             prlist_with_sep pr_comma (fun (cl,na) ->
-	       pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
-	     l)
-  | TacGeneralizeDep c ->
-      hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
-             pr_constrarg c)
-  | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
-      hov 1 (str "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
-  | TacLetTac (na,c,cl,b,e) ->
-      hov 1 ((if b then str "set" else str "remember") ++
-             (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
-              else pr_pose_as_style pr.pr_constr na c) ++
-             pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
-             pr_clauses (Some b) pr.pr_name cl)
-(*  | TacInstantiate (n,c,ConclLocation ()) ->
-      hov 1 (str "instantiate" ++ spc() ++
-             hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
-                    pr_lconstrarg c ++ str ")" ))
-  | TacInstantiate (n,c,HypLocation (id,hloc)) ->
-      hov 1 (str "instantiate" ++ spc() ++
-             hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
-                    pr_lconstrarg c ++ str ")" )
-	     ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None)))
-*)
-  (* Derived basic tactics *)
-  | TacInductionDestruct (isrec,ev,(l,el)) ->
-      hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
-             spc () ++
-             prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
-	       pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
-	       pr_with_induction_names pr.pr_dconstr ids ++
-	     pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++
-             pr_opt pr_eliminator el)
-  | TacDoubleInduction (h1,h2) ->
-      hov 1
-        (str "double induction" ++
-         pr_arg pr_quantified_hypothesis h1 ++
-	 pr_arg pr_quantified_hypothesis h2)
-  (* Automation tactics *)
-  | TacTrivial (_,[],Some []) as x -> pr_atom0 x
-  | TacTrivial (d,lems,db) ->
-      hov 0 (str (string_of_debug d ^ "trivial") ++
-             pr_auto_using pr.pr_constr lems ++ pr_hintbases db)
-  | TacAuto (_,None,[],Some []) as x -> pr_atom0 x
-  | TacAuto (d,n,lems,db) ->
-      hov 0 (str (string_of_debug d ^ "auto") ++
-	     pr_opt (pr_or_var int) n ++
-             pr_auto_using pr.pr_constr lems ++ pr_hintbases db)
-
-  (* Context management *)
-  | TacClear (true,[]) as t -> pr_atom0 t
-  | TacClear (keep,l) ->
-      hov 1 (str "clear" ++ spc () ++ (if keep then str "- " else mt ()) ++
-             prlist_with_sep spc pr.pr_name l)
-  | TacClearBody l ->
-      hov 1 (str "clearbody" ++ spc () ++ prlist_with_sep spc pr.pr_name l)
-  | TacMove (b,id1,id2) ->
-      (* Rem: only b = true is available for users *)
-      assert b;
-      hov 1
-        (str "move" ++ brk (1,1) ++ pr.pr_name id1 ++
-	 Miscprint.pr_move_location pr.pr_name id2)
-  | TacRename l ->
-      hov 1
-        (str "rename" ++ brk (1,1) ++
-         prlist_with_sep
-	   (fun () -> str "," ++ brk (1,1))
-	   (fun (i1,i2) ->
-	      pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2)
-	   l)
-
-  (* Constructors *)
-  | TacSplit (ev,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l)
-  (* Conversion *)
-  | TacReduce (r,h) ->
-      hov 1 (pr_red_expr r ++
-             pr_clauses (Some true) pr.pr_name h)
-  | TacChange (op,c,h) ->
-      hov 1 (str "change" ++ brk (1,1) ++
-      (match op with
-          None -> mt()
-        | Some p -> pr.pr_pattern p ++ spc () ++ str "with ") ++
-      pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h)
-
-  (* Equivalence relations *)
-  | TacSymmetry cls -> str "symmetry" ++ pr_clauses (Some true) pr.pr_name cls
-
-  (* Equality and inversion *)
-  | TacRewrite (ev,l,cl,by) ->
-      hov 1 (str (with_evars ev "rewrite") ++ spc () ++
-	     prlist_with_sep
-	     (fun () -> str ","++spc())
-	     (fun (b,m,c) ->
-		pr_orient b ++ pr_multi m ++
-                pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
-	     l
-	     ++ pr_clauses (Some true) pr.pr_name cl
-	     ++	(match by with Some by -> pr_by_tactic (pr.pr_tactic ltop) by | None -> mt()))
-  | TacInversion (DepInversion (k,c,ids),hyp) ->
-      hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
-      pr_quantified_hypothesis hyp ++
-      pr_with_inversion_names pr.pr_dconstr ids ++ pr_with_constr pr.pr_constr c)
-  | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
-      hov 1 (pr_induction_kind k ++ spc () ++
-      pr_quantified_hypothesis hyp ++
-      pr_with_inversion_names pr.pr_dconstr ids ++ pr_simple_hyp_clause pr.pr_name cl)
-  | TacInversion (InversionUsing (c,cl),hyp) ->
-      hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++
-      spc () ++ str "using" ++ spc () ++ pr.pr_constr c ++
-      pr_simple_hyp_clause pr.pr_name cl)
-
-in
-
-let rec pr_tac inherited tac =
-  let (strm,prec) = match tac with
-  | TacAbstract (t,None) ->
-      str "abstract " ++ pr_tac (labstract,L) t, labstract
-  | TacAbstract (t,Some s) ->
-      hov 0
-       (str "abstract (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () ++
-        str "using " ++ pr_id s),
-      labstract
-  | TacLetIn (recflag,llc,u) ->
-      let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in
-      v 0
-       (hv 0 (pr_let_clauses recflag (pr_tac ltop) llc ++ str " in") ++
-       fnl () ++ pr_tac (llet,E) u),
-      llet
-  | TacMatch (lz,t,lrul) ->
-      hov 0 (pr_lazy lz ++ str "match " ++ pr_tac ltop t ++ str " with"
-        ++ prlist
-	  (fun r -> fnl () ++ str "| " ++
-            pr_match_rule true (pr_tac ltop) pr.pr_lpattern r)
-	lrul
-        ++ fnl() ++ str "end"),
-      lmatch
-  | TacMatchGoal (lz,lr,lrul) ->
-      hov 0 (pr_lazy lz ++
-	str (if lr then "match reverse goal with" else "match goal with")
-	++ prlist
-	  (fun r -> fnl () ++ str "| " ++
-            pr_match_rule false (pr_tac ltop) pr.pr_lpattern r)
-	lrul
-        ++ fnl() ++ str "end"),
-      lmatch
-  | TacFun (lvar,body) ->
-      hov 2 (str "fun" ++
-        prlist pr_funvar lvar ++ str " =>" ++ spc () ++
-        pr_tac (lfun,E) body),
-      lfun
-  | TacThens (t,tl) ->
-      hov 1 (pr_tac (lseq,E) t ++ pr_then () ++ spc () ++
-             pr_seq_body (pr_opt_tactic (pr_tac ltop)) tl),
-      lseq
-  | TacThen (t1,t2) ->
-      hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
-             pr_tac (lseq,L) t2),
-      lseq
-  | TacDispatch tl -> pr_dispatch (pr_tac ltop) tl , lseq
-  | TacExtendTac (tf,t,tr) -> pr_tac_extend (pr_tac ltop) tf t tr , lseq
-  | TacThens3parts (t1,tf,t2,tl) ->
-      hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
-             pr_then_gen (pr_tac ltop) tf t2 tl),
-      lseq
-  | TacTry t ->
-      hov 1 (str "try" ++ spc () ++ pr_tac (ltactical,E) t),
-      ltactical
-  | TacDo (n,t) ->
-      hov 1 (str "do " ++ pr_or_var int n ++ spc () ++
-             pr_tac (ltactical,E) t),
-      ltactical
-  | TacTimeout (n,t) ->
-      hov 1 (str "timeout " ++ pr_or_var int n ++ spc () ++
-             pr_tac (ltactical,E) t),
-      ltactical
-  | TacTime (s,t) ->
-      hov 1 (str "time" ++ pr_opt str s ++ str " " ++ pr_tac (ltactical,E) t),
-      ltactical
-  | TacRepeat t ->
-      hov 1 (str "repeat" ++ spc () ++ pr_tac (ltactical,E) t),
-      ltactical
-  | TacProgress t ->
-      hov 1 (str "progress" ++ spc () ++ pr_tac (ltactical,E) t),
-      ltactical
-  | TacShowHyps t ->
-      hov 1 (str "infoH" ++ spc () ++ spc () ++ pr_tac (ltactical,E) t),
-      ltactical
-  | TacInfo t ->
-      hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t),
-      linfo
-  | TacOr (t1,t2) ->
-      hov 1 (pr_tac (lorelse,L) t1 ++ str " +" ++ brk (1,1) ++
-             pr_tac (lorelse,E) t2),
-      lorelse
-  | TacOnce t ->
-      hov 1 (str "once" ++ spc () ++ pr_tac (ltactical,E) t),
-      ltactical
-  | TacExactlyOnce t ->
-      hov 1 (str "exactly_once" ++ spc () ++ pr_tac (ltactical,E) t),
-      ltactical
-  | TacOrelse (t1,t2) ->
-      hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
-             pr_tac (lorelse,E) t2),
-      lorelse
-  | TacFail (n,l) ->
-      let arg = match n with ArgArg 0 -> mt () | _ -> pr_arg (pr_or_var int) n in
-      hov 1 (str "fail" ++ arg ++
-      prlist (pr_arg (pr_message_token pr.pr_name)) l), latom
-  | TacFirst tl ->
-      str "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
-  | TacSolve tl ->
-      str "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
-  | TacComplete t ->
-      pr_tac (lcomplete,E) t, lcomplete
-  | TacId l ->
-      str "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
-  | TacAtom (loc,t) ->
-      pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom
-  | TacArg(_,Tacexp e) -> pr.pr_tactic (latom,E) e, latom
-  | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
-      str "constr:" ++ pr.pr_constr c, latom
-  | TacArg(_,ConstrMayEval c) ->
-      pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
-  | TacArg(_,TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom
-  | TacArg(_,TacGeneric arg) -> pr.pr_generic arg, latom
-  | TacArg(_,TacCall(loc,f,[])) -> pr.pr_reference f, latom
-  | TacArg(_,TacCall(loc,f,l)) ->
-      pr_with_comments loc
-        (hov 1 (pr.pr_reference f ++ spc () ++
-         prlist_with_sep spc pr_tacarg l)),
-      lcall
-  | TacArg (_,a) -> pr_tacarg a, latom
-  | TacML (loc,s,l) ->
-      pr_with_comments loc (pr.pr_extend 1 s l), lcall
-  | TacAlias (loc,kn,l) ->
-      pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom
-  in
-  if prec_less prec inherited then strm
-  else str"(" ++ strm ++ str")"
-
-and pr_tacarg = function
-  | TacDynamic (loc,t) ->
-      pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
-  | MetaIdArg (loc,true,s) -> pr_with_comments loc (str ("$" ^ s))
-  | MetaIdArg (loc,false,s) -> pr_with_comments loc (str ("constr: $" ^ s))
-  | Reference r -> pr.pr_reference r
-  | ConstrMayEval c -> pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
-  | UConstr c -> str"uconstr:" ++ pr.pr_uconstr c
-  | TacFreshId l -> str "fresh" ++ pr_fresh_ids l
-  | TacPretype c -> str "type_term" ++ pr.pr_constr c
-  | TacNumgoals -> str "numgoals"
-  | (TacCall _|Tacexp _ | TacGeneric _) as a ->
-      str "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
-
-in pr_tac
-
-let strip_prod_binders_glob_constr n (ty,_) =
-  let rec strip_ty acc n ty =
-    if Int.equal n 0 then (List.rev acc, (ty,None)) else
-      match ty with
-          Glob_term.GProd(loc,na,Explicit,a,b) ->
-            strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b
-        | _ -> error "Cannot translate fix tactic: not enough products" in
-  strip_ty [] n ty
-
-let raw_printers =
+  type 'a printer = {
+    pr_tactic : tolerability -> 'tacexpr -> std_ppcmds;
+    pr_constr : 'trm -> std_ppcmds;
+    pr_uconstr: 'utrm -> std_ppcmds;
+    pr_lconstr : 'trm -> std_ppcmds;
+    pr_dconstr: 'dtrm -> std_ppcmds;
+    pr_pattern : 'pat -> std_ppcmds;
+    pr_lpattern : 'pat -> std_ppcmds;
+    pr_constant : 'cst -> std_ppcmds;
+    pr_reference : 'ref -> std_ppcmds;
+    pr_name : 'nam -> std_ppcmds;
+    pr_generic : 'lev generic_argument -> std_ppcmds;
+    pr_extend : int -> ml_tactic_name -> 'lev generic_argument list -> std_ppcmds;
+    pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds;
+  }
+
+  constraint 'a = <
+      term:'trm;
+      utrm:'utrm;
+      dterm:'dtrm;
+      pattern:'pat;
+      constant:'cst;
+      reference:'ref;
+      name:'nam;
+      tacexpr:'tacexpr;
+      level:'lev
+    >
+
+    let make_pr_tac pr strip_prod_binders =
+
+        (* some shortcuts *)
+        let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in
+        let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in
+        let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
+        let pr_with_bindings_arg_full = pr_with_bindings_arg in
+        let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
+        let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
+
+        let pr_constrarg c = spc () ++ pr.pr_constr c in
+        let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
+        let pr_intarg n = spc () ++ int n in
+
+        (* Some printing combinators *)
+        let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in
+
+        let extract_binders = function
+          | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
+          | body -> ([],body) in
+
+        let pr_binder_fix (nal,t) =
+          (*  match t with
+              | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
+              | _ ->*)
+          let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
+          spc() ++ hov 1 (str"(" ++ s ++ str")") in
+
+        let pr_fix_tac (id,n,c) =
+          let rec set_nth_name avoid n = function
+          (nal,ty)::bll ->
+            if n <= List.length nal then
+              match List.chop (n-1) nal with
+                  _, (_,Name id) :: _ -> id, (nal,ty)::bll
+                | bef, (loc,Anonymous) :: aft ->
+                  let id = next_ident_away (Id.of_string"y") avoid in
+                  id, ((bef@(loc,Name id)::aft, ty)::bll)
+                | _ -> assert false
+            else
+              let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
+              (id,(nal,ty)::bll')
+            | [] -> assert false in
+          let (bll,ty) = strip_prod_binders n c in
+          let names =
+            List.fold_left
+              (fun ln (nal,_) -> List.fold_left
+                (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
+                ln nal)
+              [] bll in
+          let idarg,bll = set_nth_name names n bll in
+          let annot = match names with
+            | [_] -> mt ()
+            | _ -> spc() ++ str"{struct " ++ pr_id idarg ++ str"}"
+          in
+          hov 1 (str"(" ++ pr_id id ++
+                   prlist pr_binder_fix bll ++ annot ++ str" :" ++
+                   pr_lconstrarg ty ++ str")") in
+        (*  spc() ++
+            hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+            c)
+        *)
+        let pr_cofix_tac (id,c) =
+          hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
+
+        (* Printing tactics as arguments *)
+        let rec pr_atom0 = function
+          | TacIntroPattern [] -> str "intros"
+          | TacIntroMove (None,MoveLast) -> str "intro"
+          | TacTrivial (d,[],Some []) -> str (string_of_debug d ^ "trivial")
+          | TacAuto (d,None,[],Some []) -> str (string_of_debug d ^ "auto")
+          | TacClear (true,[]) -> str "clear"
+          | t -> str "(" ++ pr_atom1 t ++ str ")"
+
+        (* Main tactic printer *)
+        and pr_atom1 = function
+          (* Basic tactics *)
+          | TacIntroPattern [] as t -> pr_atom0 t
+          | TacIntroPattern (_::_ as p) ->
+            hov 1 (str "intros" ++ spc () ++
+                     prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
+          | 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 ++
+                     Miscprint.pr_move_location pr.pr_name hto)
+          | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
+          | TacApply (a,ev,cb,inhyp) ->
+            hov 1 ((if a then mt() else str "simple ") ++
+                      str (with_evars ev "apply") ++ spc () ++
+                      prlist_with_sep pr_comma pr_with_bindings_arg cb ++
+                      pr_in_hyp_as pr.pr_dconstr pr.pr_name inhyp)
+          | TacElim (ev,cb,cbo) ->
+            hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings_arg cb ++
+                     pr_opt pr_eliminator cbo)
+          | TacCase (ev,cb) ->
+            hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
+          | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
+          | TacMutualFix (id,n,l) ->
+            hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
+                     str"with " ++ prlist_with_sep spc pr_fix_tac l)
+          | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
+          | TacMutualCofix (id,l) ->
+            hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
+                     str"with " ++ prlist_with_sep spc pr_cofix_tac l)
+          | TacAssert (b,Some tac,ipat,c) ->
+            hov 1 (str (if b then "assert" else "enough") ++
+                     pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
+                     pr_by_tactic (pr.pr_tactic ltop) tac)
+          | TacAssert (_,None,ipat,c) ->
+            hov 1 (str "pose proof" ++
+                     pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c)
+          | TacGeneralize l ->
+            hov 1 (str "generalize" ++ spc () ++
+                     prlist_with_sep pr_comma (fun (cl,na) ->
+                       pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
+                     l)
+          | TacGeneralizeDep c ->
+            hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
+                     pr_constrarg c)
+          | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
+            hov 1 (str "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+          | TacLetTac (na,c,cl,b,e) ->
+            hov 1 ((if b then str "set" else str "remember") ++
+                      (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
+                       else pr_pose_as_style pr.pr_constr na c) ++
+                      pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
+                      pr_clauses (Some b) pr.pr_name cl)
+          (*  | TacInstantiate (n,c,ConclLocation ()) ->
+              hov 1 (str "instantiate" ++ spc() ++
+              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+              pr_lconstrarg c ++ str ")" ))
+              | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+              hov 1 (str "instantiate" ++ spc() ++
+              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+              pr_lconstrarg c ++ str ")" )
+              ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None)))
+          *)
+
+          (* Derived basic tactics *)
+          | TacInductionDestruct (isrec,ev,(l,el)) ->
+            hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
+                     spc () ++
+                     prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
+                       pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
+                         pr_with_induction_names pr.pr_dconstr ids ++
+                         pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++
+                     pr_opt pr_eliminator el)
+          | TacDoubleInduction (h1,h2) ->
+            hov 1
+              (str "double induction" ++
+                 pr_arg pr_quantified_hypothesis h1 ++
+                 pr_arg pr_quantified_hypothesis h2)
+
+          (* Automation tactics *)
+          | TacTrivial (_,[],Some []) as x -> pr_atom0 x
+          | TacTrivial (d,lems,db) ->
+            hov 0 (str (string_of_debug d ^ "trivial") ++
+                     pr_auto_using pr.pr_constr lems ++ pr_hintbases db)
+          | TacAuto (_,None,[],Some []) as x -> pr_atom0 x
+          | TacAuto (d,n,lems,db) ->
+            hov 0 (str (string_of_debug d ^ "auto") ++
+                     pr_opt (pr_or_var int) n ++
+                     pr_auto_using pr.pr_constr lems ++ pr_hintbases db)
+
+          (* Context management *)
+          | TacClear (true,[]) as t -> pr_atom0 t
+          | TacClear (keep,l) ->
+            hov 1 (str "clear" ++ spc () ++ (if keep then str "- " else mt ()) ++
+                     prlist_with_sep spc pr.pr_name l)
+          | TacClearBody l ->
+            hov 1 (str "clearbody" ++ spc () ++ prlist_with_sep spc pr.pr_name l)
+          | TacMove (b,id1,id2) ->
+            (* Rem: only b = true is available for users *)
+            assert b;
+            hov 1
+              (str "move" ++ brk (1,1) ++ pr.pr_name id1 ++
+                 Miscprint.pr_move_location pr.pr_name id2)
+          | TacRename l ->
+            hov 1
+              (str "rename" ++ brk (1,1) ++
+                 prlist_with_sep
+                 (fun () -> str "," ++ brk (1,1))
+                 (fun (i1,i2) ->
+                   pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2)
+                 l)
+
+          (* Constructors *)
+          | TacSplit (ev,l) ->
+            hov 1 (str (with_evars ev "exists")
+                   ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l)
+
+          (* Conversion *)
+          | TacReduce (r,h) ->
+            hov 1 (pr_red_expr r ++
+                     pr_clauses (Some true) pr.pr_name h)
+          | TacChange (op,c,h) ->
+            hov 1 (str "change" ++ brk (1,1) ++
+                     (match op with
+                         None -> mt()
+                       | Some p -> pr.pr_pattern p ++ spc () ++ str "with ") ++
+                     pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h)
+
+          (* Equivalence relations *)
+          | TacSymmetry cls -> str "symmetry" ++ pr_clauses (Some true) pr.pr_name cls
+
+          (* Equality and inversion *)
+          | TacRewrite (ev,l,cl,by) ->
+            hov 1 (str (with_evars ev "rewrite") ++ spc () ++
+                     prlist_with_sep
+                     (fun () -> str ","++spc())
+                     (fun (b,m,c) ->
+                       pr_orient b ++ pr_multi m ++
+                         pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
+                     l
+                   ++ pr_clauses (Some true) pr.pr_name cl
+                   ++ (match by with Some by -> pr_by_tactic (pr.pr_tactic ltop) by | None -> mt()))
+          | TacInversion (DepInversion (k,c,ids),hyp) ->
+            hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
+                     pr_quantified_hypothesis hyp ++
+                     pr_with_inversion_names pr.pr_dconstr ids ++ pr_with_constr pr.pr_constr c)
+          | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
+            hov 1 (pr_induction_kind k ++ spc () ++
+                     pr_quantified_hypothesis hyp ++
+                     pr_with_inversion_names pr.pr_dconstr ids ++ pr_simple_hyp_clause pr.pr_name cl)
+          | TacInversion (InversionUsing (c,cl),hyp) ->
+            hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++
+                     spc () ++ str "using" ++ spc () ++ pr.pr_constr c ++
+                     pr_simple_hyp_clause pr.pr_name cl)
+
+        in
+
+        let rec pr_tac inherited tac =
+          let (strm,prec) = match tac with
+            | TacAbstract (t,None) ->
+              str "abstract " ++ pr_tac (labstract,L) t, labstract
+            | TacAbstract (t,Some s) ->
+              hov 0
+                (str "abstract (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () ++
+                   str "using " ++ pr_id s),
+              labstract
+            | TacLetIn (recflag,llc,u) ->
+              let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in
+              v 0
+                (hv 0 (pr_let_clauses recflag (pr_tac ltop) llc ++ str " in") ++
+                   fnl () ++ pr_tac (llet,E) u),
+              llet
+            | TacMatch (lz,t,lrul) ->
+              hov 0 (pr_lazy lz ++ str "match " ++ pr_tac ltop t ++ str " with"
+                     ++ prlist
+                       (fun r -> fnl () ++ str "| " ++
+                         pr_match_rule true (pr_tac ltop) pr.pr_lpattern r)
+                       lrul
+                     ++ fnl() ++ str "end"),
+              lmatch
+            | TacMatchGoal (lz,lr,lrul) ->
+              hov 0 (pr_lazy lz ++
+                       str (if lr then "match reverse goal with" else "match goal with")
+                     ++ prlist
+                       (fun r -> fnl () ++ str "| " ++
+                         pr_match_rule false (pr_tac ltop) pr.pr_lpattern r)
+                       lrul
+                     ++ fnl() ++ str "end"),
+              lmatch
+            | TacFun (lvar,body) ->
+              hov 2 (str "fun" ++
+                       prlist pr_funvar lvar ++ str " =>" ++ spc () ++
+                       pr_tac (lfun,E) body),
+              lfun
+            | TacThens (t,tl) ->
+              hov 1 (pr_tac (lseq,E) t ++ pr_then () ++ spc () ++
+                       pr_seq_body (pr_opt_tactic (pr_tac ltop)) tl),
+              lseq
+            | TacThen (t1,t2) ->
+              hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
+                       pr_tac (lseq,L) t2),
+              lseq
+            | TacDispatch tl -> pr_dispatch (pr_tac ltop) tl , lseq
+            | TacExtendTac (tf,t,tr) -> pr_tac_extend (pr_tac ltop) tf t tr , lseq
+            | TacThens3parts (t1,tf,t2,tl) ->
+              hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
+                       pr_then_gen (pr_tac ltop) tf t2 tl),
+              lseq
+            | TacTry t ->
+              hov 1 (str "try" ++ spc () ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacDo (n,t) ->
+              hov 1 (str "do " ++ pr_or_var int n ++ spc () ++
+                       pr_tac (ltactical,E) t),
+              ltactical
+            | TacTimeout (n,t) ->
+              hov 1 (str "timeout " ++ pr_or_var int n ++ spc () ++
+                       pr_tac (ltactical,E) t),
+              ltactical
+            | TacTime (s,t) ->
+              hov 1 (str "time" ++ pr_opt str s ++ str " " ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacRepeat t ->
+              hov 1 (str "repeat" ++ spc () ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacProgress t ->
+              hov 1 (str "progress" ++ spc () ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacShowHyps t ->
+              hov 1 (str "infoH" ++ spc () ++ spc () ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacInfo t ->
+              hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t),
+              linfo
+            | TacOr (t1,t2) ->
+              hov 1 (pr_tac (lorelse,L) t1 ++ str " +" ++ brk (1,1) ++
+                       pr_tac (lorelse,E) t2),
+              lorelse
+            | TacOnce t ->
+              hov 1 (str "once" ++ spc () ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacExactlyOnce t ->
+              hov 1 (str "exactly_once" ++ spc () ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacOrelse (t1,t2) ->
+              hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
+                       pr_tac (lorelse,E) t2),
+              lorelse
+            | TacFail (n,l) ->
+              let arg = match n with ArgArg 0 -> mt () | _ -> pr_arg (pr_or_var int) n in
+              hov 1 (str "fail" ++ arg ++
+                       prlist (pr_arg (pr_message_token pr.pr_name)) l), latom
+            | TacFirst tl ->
+              str "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
+            | TacSolve tl ->
+              str "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
+            | TacComplete t ->
+              pr_tac (lcomplete,E) t, lcomplete
+            | TacId l ->
+              str "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
+            | TacAtom (loc,t) ->
+              pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom
+            | TacArg(_,Tacexp e) -> pr.pr_tactic (latom,E) e, latom
+            | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
+              str "constr:" ++ pr.pr_constr c, latom
+            | TacArg(_,ConstrMayEval c) ->
+              pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
+            | TacArg(_,TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom
+            | TacArg(_,TacGeneric arg) -> pr.pr_generic arg, latom
+            | TacArg(_,TacCall(loc,f,[])) -> pr.pr_reference f, latom
+            | TacArg(_,TacCall(loc,f,l)) ->
+              pr_with_comments loc
+                (hov 1 (pr.pr_reference f ++ spc () ++
+                          prlist_with_sep spc pr_tacarg l)),
+              lcall
+            | TacArg (_,a) -> pr_tacarg a, latom
+            | TacML (loc,s,l) ->
+              pr_with_comments loc (pr.pr_extend 1 s l), lcall
+            | TacAlias (loc,kn,l) ->
+              pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom
+          in
+          if prec_less prec inherited then strm
+          else str"(" ++ strm ++ str")"
+
+        and pr_tacarg = function
+          | TacDynamic (loc,t) ->
+            pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
+          | MetaIdArg (loc,true,s) -> pr_with_comments loc (str ("$" ^ s))
+          | MetaIdArg (loc,false,s) -> pr_with_comments loc (str ("constr: $" ^ s))
+          | Reference r -> pr.pr_reference r
+          | ConstrMayEval c -> pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
+          | UConstr c -> str"uconstr:" ++ pr.pr_uconstr c
+          | TacFreshId l -> str "fresh" ++ pr_fresh_ids l
+          | TacPretype c -> str "type_term" ++ pr.pr_constr c
+          | TacNumgoals -> str "numgoals"
+          | (TacCall _|Tacexp _ | TacGeneric _) as a ->
+            str "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
+
+        in pr_tac
+
+  let strip_prod_binders_glob_constr n (ty,_) =
+    let rec strip_ty acc n ty =
+      if Int.equal n 0 then (List.rev acc, (ty,None)) else
+        match ty with
+            Glob_term.GProd(loc,na,Explicit,a,b) ->
+              strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b
+          | _ -> error "Cannot translate fix tactic: not enough products" in
+    strip_ty [] n ty
+
+  let raw_printers =
     (strip_prod_binders_expr)
 
-let rec pr_raw_tactic_level n (t:raw_tactic_expr) =
-  let pr = {
-    pr_tactic = pr_raw_tactic_level;
-    pr_constr = pr_constr_expr;
-    pr_uconstr = pr_constr_expr;
-    pr_dconstr = pr_constr_expr;
-    pr_lconstr = pr_lconstr_expr;
-    pr_pattern = pr_constr_pattern_expr;
-    pr_lpattern = pr_lconstr_pattern_expr;
-    pr_constant = pr_or_by_notation pr_reference;
-    pr_reference = pr_reference;
-    pr_name = pr_lident;
-    pr_generic = Genprint.generic_raw_print;
-    pr_extend = pr_raw_extend 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
-  make_pr_tac pr raw_printers n t
-
-let pr_raw_tactic = pr_raw_tactic_level ltop
-
-let pr_and_constr_expr pr (c,_) = pr c
-
-let pr_pat_and_constr_expr pr ((c,_),_) = pr c
-
-let rec pr_glob_tactic_level env n t =
-  let glob_printers =
-    (strip_prod_binders_glob_constr)
-  in
-  let rec prtac n (t:glob_tactic_expr) =
+  let rec pr_raw_tactic_level n (t:raw_tactic_expr) =
     let pr = {
-      pr_tactic = prtac;
-      pr_constr = pr_and_constr_expr (pr_glob_constr_env env);
-      pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env);
-      pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
-      pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env);
-      pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
-      pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
-      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_tactic = pr_raw_tactic_level;
+      pr_constr = pr_constr_expr;
+      pr_uconstr = pr_constr_expr;
+      pr_dconstr = pr_constr_expr;
+      pr_lconstr = pr_lconstr_expr;
+      pr_pattern = pr_constr_pattern_expr;
+      pr_lpattern = pr_lconstr_pattern_expr;
+      pr_constant = pr_or_by_notation pr_reference;
+      pr_reference = pr_reference;
       pr_name = pr_lident;
-      pr_generic = Genprint.generic_glb_print;
-      pr_extend = pr_glob_extend
-        (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_alias = pr_glob_alias
-        (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 = Genprint.generic_raw_print;
+      pr_extend = pr_raw_extend 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
-    make_pr_tac pr glob_printers n t
-  in
-  prtac n t
+    make_pr_tac pr raw_printers n t
 
-let pr_glob_tactic env = pr_glob_tactic_level env ltop
+  let pr_raw_tactic = pr_raw_tactic_level ltop
 
+  let pr_and_constr_expr pr (c,_) = pr c
 
-let strip_prod_binders_constr n ty =
-  let rec strip_ty acc n ty =
-    if n=0 then (List.rev acc, ty) else
-      match Term.kind_of_term ty with
-          Term.Prod(na,a,b) ->
-            strip_ty (([Loc.ghost,na],a)::acc) (n-1) b
-        | _ -> error "Cannot translate fix tactic: not enough products" in
-  strip_ty [] n ty
+  let pr_pat_and_constr_expr pr ((c,_),_) = pr c
 
-let pr_tactic_level env n t =
-  let typed_printers =
-    (strip_prod_binders_constr)
-  in
-  let prtac n (t:tactic_expr) =
-    let pr = {
-      pr_tactic = pr_glob_tactic_level env;
-      pr_constr = pr_constr_env env Evd.empty;
-      pr_uconstr = (fun _ -> mt ()); (* arnaud: todo *)
-      pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
-      pr_lconstr = pr_lconstr_env env Evd.empty;
-      pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
-      pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
-      pr_constant = pr_and_short_name (pr_evaluable_reference_env env);
-      pr_reference = pr_located pr_ltac_constant;
-      pr_name = pr_id;
-      pr_generic = Genprint.generic_top_print;
-      pr_extend = pr_extend
-        (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
-        (pr_glob_tactic_level env) pr_constr_pattern;
-      pr_alias = pr_alias
-        (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
-        (pr_glob_tactic_level env) pr_constr_pattern;
-    }
+  let rec pr_glob_tactic_level env n t =
+    let glob_printers =
+      (strip_prod_binders_glob_constr)
+    in
+    let rec prtac n (t:glob_tactic_expr) =
+      let pr = {
+        pr_tactic = prtac;
+        pr_constr = pr_and_constr_expr (pr_glob_constr_env env);
+        pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env);
+        pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
+        pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env);
+        pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
+        pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
+        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 = Genprint.generic_glb_print;
+        pr_extend = pr_glob_extend
+          (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_alias = pr_glob_alias
+          (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));
+      } in
+      make_pr_tac pr glob_printers n t
     in
-    make_pr_tac pr typed_printers n t
-  in
-  prtac n t
+    prtac n t
+
+  let pr_glob_tactic env = pr_glob_tactic_level env ltop
+
+
+  let strip_prod_binders_constr n ty =
+    let rec strip_ty acc n ty =
+      if n=0 then (List.rev acc, ty) else
+        match Term.kind_of_term ty with
+            Term.Prod(na,a,b) ->
+              strip_ty (([Loc.ghost,na],a)::acc) (n-1) b
+          | _ -> error "Cannot translate fix tactic: not enough products" in
+    strip_ty [] n ty
+
+  let pr_tactic_level env n t =
+    let typed_printers =
+      (strip_prod_binders_constr)
+    in
+    let prtac n (t:tactic_expr) =
+      let pr = {
+        pr_tactic = pr_glob_tactic_level env;
+        pr_constr = pr_constr_env env Evd.empty;
+        pr_uconstr = (fun _ -> mt ()); (* arnaud: todo *)
+        pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
+        pr_lconstr = pr_lconstr_env env Evd.empty;
+        pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
+        pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
+        pr_constant = pr_and_short_name (pr_evaluable_reference_env env);
+        pr_reference = pr_located pr_ltac_constant;
+        pr_name = pr_id;
+        pr_generic = Genprint.generic_top_print;
+        pr_extend = pr_extend
+          (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
+          (pr_glob_tactic_level env) pr_constr_pattern;
+        pr_alias = pr_alias
+          (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
+          (pr_glob_tactic_level env) pr_constr_pattern;
+      }
+      in
+      make_pr_tac pr typed_printers n t
+    in
+    prtac n t
+
+  let pr_tactic env = pr_tactic_level env ltop
 
-let pr_tactic env = pr_tactic_level env ltop
+end
 
+include Make (Ppconstr)
 
 (** Registering *)