printing/Ppannotation: New annotation for tactic syntactic objects.

printing/Pptactic: Tag tactics pretty-printing.
printing/Ppvernac: Use the relevent Pptactic pretty-printer.
printing/RichPrinter: Publish two new services.

8 files changed, 586 insertions, 339 deletions

diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
index 60d5da413..5f9dcdc99 100644
--- a/printing/ppannotation.ml
+++ b/printing/ppannotation.ml
@@ -9,18 +9,31 @@
 open Ppextend
 open Constrexpr
 open Vernacexpr
+open Tacexpr
 
 type t =
   | AKeyword
-  | AUnparsing  of unparsing
-  | AConstrExpr of constr_expr
-  | AVernac     of vernac_expr
+  | AUnparsing            of unparsing
+  | AConstrExpr           of constr_expr
+  | AVernac               of vernac_expr
+  | AGlobTacticExpr       of glob_tactic_expr
+  | AGlobAtomicTacticExpr of glob_atomic_tactic_expr
+  | ARawTacticExpr        of raw_tactic_expr
+  | ARawAtomicTacticExpr  of raw_atomic_tactic_expr
+  | ATacticExpr           of tactic_expr
+  | AAtomicTacticExpr     of atomic_tactic_expr
 
 let tag_of_annotation = function
-  | AKeyword      -> "keyword"
-  | AUnparsing _  -> "unparsing"
-  | AConstrExpr _ -> "constr_expr"
-  | AVernac _     -> "vernac_expr"
+  | AKeyword                -> "keyword"
+  | AUnparsing _            -> "unparsing"
+  | AConstrExpr _           -> "constr_expr"
+  | AVernac _               -> "vernac_expr"
+  | AGlobTacticExpr _       -> "glob_tactic_expr"
+  | AGlobAtomicTacticExpr _ -> "glob_atomic_tactic_expr"
+  | ARawTacticExpr _        -> "raw_tactic_expr"
+  | ARawAtomicTacticExpr _  -> "raw_atomic_tactic_expr"
+  | ATacticExpr _           -> "tactic_expr"
+  | AAtomicTacticExpr _     -> "atomic_tactic_expr"
 
 let attributes_of_annotation a =
   []
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
index d10bc5a57..9e3ab2b0e 100644
--- a/printing/ppannotation.mli
+++ b/printing/ppannotation.mli
@@ -12,12 +12,19 @@
 open Ppextend
 open Constrexpr
 open Vernacexpr
+open Tacexpr
 
 type t =
   | AKeyword
-  | AUnparsing  of unparsing
-  | AConstrExpr of constr_expr
-  | AVernac     of vernac_expr
+  | AUnparsing            of unparsing
+  | AConstrExpr           of constr_expr
+  | AVernac               of vernac_expr
+  | AGlobTacticExpr       of glob_tactic_expr
+  | AGlobAtomicTacticExpr of glob_atomic_tactic_expr
+  | ARawTacticExpr        of raw_tactic_expr
+  | ARawAtomicTacticExpr  of raw_atomic_tactic_expr
+  | ATacticExpr           of tactic_expr
+  | AAtomicTacticExpr     of atomic_tactic_expr
 
 val tag_of_annotation : t -> string
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 645a3409e..ad3f95ef2 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -24,60 +24,81 @@ open Genredexpr
 open Ppconstr
 open Printer
 
-module Make (Ppconstr : Ppconstrsig.Pp) =
-struct
-
-  let pr_global x = Nametab.pr_global_env Id.Set.empty x
-
-  type grammar_terminals = string option list
-
-  type pp_tactic = {
-    pptac_args : argument_type list;
-    pptac_prods : int * grammar_terminals;
-  }
-
-  (* ML Extensions *)
-  let prtac_tab = Hashtbl.create 17
-
-  (* Tactic notations *)
-  let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
-
-  let declare_ml_tactic_pprule key pt =
-    Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods
-
-  let declare_notation_tactic_pprule kn pt =
-    prnotation_tab := KNmap.add kn pt !prnotation_tab
-
-  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 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 extra_genarg_printer =
-      (Term.constr -> std_ppcmds) ->
-      (Term.constr -> std_ppcmds) ->
-      (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-      'a -> std_ppcmds
-
-  let genarg_pprule = ref String.Map.empty
-
-  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_global x = Nametab.pr_global_env Id.Set.empty x
+
+type grammar_terminals = string option list
+
+type pp_tactic = {
+  pptac_args : argument_type list;
+  pptac_prods : int * grammar_terminals;
+}
+
+(* ML Extensions *)
+let prtac_tab = Hashtbl.create 17
+
+(* Tactic notations *)
+let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
+
+let declare_ml_tactic_pprule key pt =
+  Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods
+
+let declare_notation_tactic_pprule kn pt =
+  prnotation_tab := KNmap.add kn pt !prnotation_tab
+
+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 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 extra_genarg_printer =
+    (Term.constr -> std_ppcmds) ->
+    (Term.constr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
+
+let genarg_pprule = ref String.Map.empty
+
+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
+
+module Make
+  (Ppconstr : Ppconstrsig.Pp)
+  (Taggers : sig
+      val tag_keyword
+        : std_ppcmds -> std_ppcmds
+      val tag_glob_tactic_expr
+        : glob_tactic_expr -> std_ppcmds -> std_ppcmds
+      val tag_glob_atomic_tactic_expr
+        : glob_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
+      val tag_raw_tactic_expr
+        : raw_tactic_expr -> std_ppcmds -> std_ppcmds
+      val tag_raw_atomic_tactic_expr
+        : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
+      val tag_tactic_expr
+        : tactic_expr -> std_ppcmds -> std_ppcmds
+      val tag_atomic_tactic_expr
+        : atomic_tactic_expr -> std_ppcmds -> std_ppcmds
+  end)
+= struct
+
+  open Taggers
+
+  let keyword x = tag_keyword (str x)
 
   let pr_arg pr x = spc () ++ pr x
 
@@ -107,10 +128,10 @@ struct
 
   let pr_bindings prc prlc = function
     | ImplicitBindings l ->
-      brk (1,1) ++ str "with" ++ brk (1,1) ++
+      brk (1,1) ++ keyword "with" ++ brk (1,1) ++
         hv 0 (prlist_with_sep spc prc l)
     | ExplicitBindings l ->
-      brk (1,1) ++ str "with" ++ brk (1,1) ++
+      brk (1,1) ++ keyword "with" ++ brk (1,1) ++
         hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l)
     | NoBindings -> mt ()
 
@@ -135,7 +156,7 @@ struct
 
   let pr_with_constr prc = function
     | None -> mt ()
-    | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
+    | Some c -> spc () ++ hov 1 (keyword "with" ++ spc () ++ prc c)
 
   let pr_message_token prid = function
     | MsgString s -> qs s
@@ -369,11 +390,11 @@ struct
   let pr_bindings_gen for_ex prc prlc = function
     | ImplicitBindings l ->
       spc () ++
-        hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++
+        hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++
                  prlist_with_sep spc prc l)
     | ExplicitBindings l ->
       spc () ++
-        hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++
+        hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++
                  pr_esubst prlc l)
     | NoBindings -> mt ()
 
@@ -383,10 +404,10 @@ struct
     hov 1 (prc c ++ pr_bindings prc prlc bl)
 
   let pr_as_disjunctive_ipat prc ipatl =
-    str "as " ++
+    keyword "as" ++ spc () ++
       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) = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
 
   let pr_with_induction_names prc = function
     | None, None -> mt ()
@@ -397,7 +418,7 @@ struct
         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)
+    spc () ++ hov 1 (keyword "as" ++ spc () ++ Miscprint.pr_intro_pattern prc ipat)
 
   let pr_with_inversion_names prc = function
     | None -> mt ()
@@ -409,7 +430,7 @@ struct
 
   let pr_as_name = function
     | Anonymous -> mt ()
-    | Name id -> str " as " ++ pr_lident (Loc.ghost,id)
+    | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.ghost,id)
 
   let pr_pose_as_style prc na c =
     spc() ++ prc c ++ pr_as_name na
@@ -436,18 +457,20 @@ struct
 
   let pr_by_tactic prt = function
     | TacId [] -> mt ()
-    | tac -> spc() ++ str "by " ++ prt tac
+    | tac -> spc() ++ keyword "by" ++ spc () ++ prt tac
 
   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
+      spc () ++ pr_with_occurrences (fun id ->
+        str "(" ++ keyword "type of" ++ spc () ++ pr_id id ++ str ")"
+      ) occs
     | occs, InHypValueOnly ->
-      spc () ++
-        pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs
+      spc () ++ pr_with_occurrences (fun id ->
+        str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")"
+      ) occs
 
-  let pr_in pp = spc () ++ hov 0 (str "in" ++ pp)
+  let pr_in pp = spc () ++ hov 0 (keyword "in" ++ pp)
 
   let pr_simple_hyp_clause pr_id = function
     | [] -> mt ()
@@ -491,20 +514,20 @@ struct
     | ElimOnAnonHyp n -> int n
 
   let pr_induction_kind = function
-    | SimpleInversion -> str "simple inversion"
-    | FullInversion -> str "inversion"
-    | FullInversionClear -> str "inversion_clear"
+    | SimpleInversion -> keyword "simple inversion"
+    | FullInversion -> keyword "inversion"
+    | FullInversionClear -> keyword "inversion_clear"
 
-  let pr_lazy lz = if lz then str "lazy" else mt ()
+  let pr_lazy lz = if lz then keyword "lazy" else mt ()
 
   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 "]"
+      keyword "context" ++ str" [" ++ pr_pat a ++ str "]"
     | Subterm (b,Some id,a) ->
-      str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+      keyword "context" ++ spc () ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
 
   let pr_match_hyps pr_pat = function
     | Hyp (nal,mp) ->
@@ -578,15 +601,15 @@ struct
             str " ]")
 
   let pr_hintbases = function
-    | None -> spc () ++ str "with *"
+    | None -> spc () ++ keyword "with" ++ str" *"
     | Some [] -> mt ()
     | Some l ->
-      spc () ++ hov 2 (str "with" ++ prlist (fun s -> spc () ++ str s) l)
+      spc () ++ hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
 
   let pr_auto_using prc = function
     | [] -> mt ()
     | l -> spc () ++
-      hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
+      hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
 
   let string_of_debug = function
     | Off -> ""
@@ -612,38 +635,38 @@ struct
 
   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 *)
+  (** 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_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;
+    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
+      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 =
+    let make_pr_tac pr strip_prod_binders tag_atom tag =
 
         (* some shortcuts *)
         let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in
@@ -658,7 +681,7 @@ struct
         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 pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in
 
         let extract_binders = function
           | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
@@ -694,8 +717,12 @@ struct
               [] 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"}"
+            | [_] ->
+              mt ()
+            | _ ->
+              spc() ++ str"{"
+              ++ keyword "struct" ++ spc ()
+              ++ pr_id idarg ++ str"}"
           in
           hov 1 (str"(" ++ pr_id id ++
                    prlist pr_binder_fix bll ++ annot ++ str" :" ++
@@ -708,68 +735,90 @@ struct
           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"
+        let rec pr_atom0 a = tag_atom a (match a with
+          | TacIntroPattern [] -> keyword "intros"
+          | TacIntroMove (None,MoveLast) -> keyword "intro"
+          | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ keyword "trivial"
+          | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ keyword "auto"
+          | TacClear (true,[]) -> keyword "clear"
           | t -> str "(" ++ pr_atom1 t ++ str ")"
+        )
 
         (* Main tactic printer *)
-        and pr_atom1 = function
+        and pr_atom1 a = tag_atom a (match a with
           (* Basic tactics *)
-          | TacIntroPattern [] as t -> pr_atom0 t
+          | TacIntroPattern [] as t ->
+            pr_atom0 t
           | TacIntroPattern (_::_ as p) ->
-            hov 1 (str "intros" ++ spc () ++
+            hov 1 (keyword "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 (None,MoveLast) as t ->
+            pr_atom0 t
+          | TacIntroMove (Some id,MoveLast) ->
+            keyword "intro" ++ spc () ++ pr_id id
           | TacIntroMove (ido,hto) ->
-            hov 1 (str"intro" ++ pr_opt pr_id ido ++
+            hov 1 (keyword "intro" ++ pr_opt pr_id ido ++
                      Miscprint.pr_move_location pr.pr_name hto)
-          | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
+          | TacExact c ->
+            hov 1 (keyword "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)
+            hov 1 (
+              (if a then mt() else keyword "simple ") ++
+                keyword (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)
+            hov 1 (
+              keyword (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)
+            hov 1 (keyword (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
+          | TacFix (ido,n) -> hov 1 (keyword "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)
+            hov 1 (
+              keyword "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
+              ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l)
+          | TacCofix ido ->
+            hov 1 (keyword "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)
+            hov 1 (
+              keyword "cofix" ++ spc () ++ pr_id id ++ spc()
+              ++ keyword "with" ++ spc () ++ 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)
+            hov 1 (
+              keyword (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)
+            hov 1 (
+              keyword "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)
+            hov 1 (
+              keyword "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)
+            hov 1 (
+              keyword "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)
+            hov 1 (keyword "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)
+            hov 1 (
+              (if b then keyword "set" else keyword "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" :=" ++
@@ -783,237 +832,340 @@ struct
 
           (* 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)
+            hov 1 (
+              keyword (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)
+            hov 1 (
+              keyword "double induction"
+              ++ pr_arg pr_quantified_hypothesis h1
+              ++ pr_arg pr_quantified_hypothesis h2
+            )
 
           (* Automation tactics *)
-          | TacTrivial (_,[],Some []) as x -> pr_atom0 x
+          | 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
+            hov 0 (
+              str (string_of_debug d) ++ keyword "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)
+            hov 0 (
+              str (string_of_debug d) ++ keyword "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 (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)
+            hov 1 (
+              keyword "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)
+            hov 1 (
+              keyword "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)
+            hov 1 (
+              keyword "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)
+            hov 1 (
+              keyword "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)
+            hov 1 (
+              keyword (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)
+            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)
+            hov 1 (
+              keyword "change" ++ brk (1,1)
+              ++ (
+                match op with
+                    None ->
+                      mt ()
+                  | Some p ->
+                    pr.pr_pattern p ++ spc ()
+                    ++ keyword "with" ++ spc ()
+              ) ++ 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
+          | TacSymmetry cls ->
+            keyword "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()))
+            hov 1 (
+              keyword (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)
+            hov 1 (
+              keyword "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)
+            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)
-
+            hov 1 (
+              keyword "inversion" ++ spc()
+              ++ pr_quantified_hypothesis hyp ++ spc ()
+              ++ keyword "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
+          let return (doc, l) = (tag tac doc, l) in
+          let (strm, prec) = return (match tac with
             | TacAbstract (t,None) ->
-              str "abstract " ++ pr_tac (labstract,L) t, labstract
+              keyword "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),
+              hov 0 (
+                keyword "abstract"
+                ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc ()
+                ++ keyword "using" ++ spc () ++ 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),
+                (hv 0 (
+                  pr_let_clauses recflag (pr_tac ltop) llc
+                  ++ spc () ++ keyword "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"),
+              hov 0 (
+                pr_lazy lz ++ keyword "match" ++ spc ()
+                ++ pr_tac ltop t ++ spc () ++ keyword "with"
+                ++ prlist (fun r ->
+                  fnl () ++ str "| "
+                  ++ pr_match_rule true (pr_tac ltop) pr.pr_lpattern r
+                ) lrul
+                ++ fnl() ++ keyword "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"),
+              hov 0 (
+                pr_lazy lz
+                ++ keyword (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() ++ keyword "end"),
               lmatch
             | TacFun (lvar,body) ->
-              hov 2 (str "fun" ++
-                       prlist pr_funvar lvar ++ str " =>" ++ spc () ++
-                       pr_tac (lfun,E) body),
+              hov 2 (
+                keyword "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),
+              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),
+              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
+            | 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),
+              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),
+              hov 1 (
+                keyword "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),
+              hov 1 (
+                str "do" ++ spc ()
+                ++ 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),
+              hov 1 (
+                keyword "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),
+              hov 1 (
+                keyword "time"
+                ++ pr_opt str s ++ spc ()
+                ++ pr_tac (ltactical,E) t),
               ltactical
             | TacRepeat t ->
-              hov 1 (str "repeat" ++ spc () ++ pr_tac (ltactical,E) t),
+              hov 1 (
+                keyword "repeat" ++ spc ()
+                ++ pr_tac (ltactical,E) t),
               ltactical
             | TacProgress t ->
-              hov 1 (str "progress" ++ spc () ++ pr_tac (ltactical,E) t),
+              hov 1 (
+                keyword "progress" ++ spc ()
+                ++ pr_tac (ltactical,E) t),
               ltactical
             | TacShowHyps t ->
-              hov 1 (str "infoH" ++ spc () ++ spc () ++ pr_tac (ltactical,E) t),
+              hov 1 (
+                keyword "infoH" ++ spc ()
+                ++ pr_tac (ltactical,E) t),
               ltactical
             | TacInfo t ->
-              hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t),
+              hov 1 (
+                keyword "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),
+              hov 1 (
+                pr_tac (lorelse,L) t1 ++ spc ()
+                ++ str "+" ++ brk (1,1)
+                ++ pr_tac (lorelse,E) t2),
               lorelse
             | TacOnce t ->
-              hov 1 (str "once" ++ spc () ++ pr_tac (ltactical,E) t),
+              hov 1 (
+                keyword "once" ++ spc ()
+                ++ pr_tac (ltactical,E) t),
               ltactical
             | TacExactlyOnce t ->
-              hov 1 (str "exactly_once" ++ spc () ++ pr_tac (ltactical,E) t),
+              hov 1 (
+                keyword "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),
+              hov 1 (
+                pr_tac (lorelse,L) t1 ++ spc ()
+                ++ 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
+              let arg =
+                match n with
+                  | ArgArg 0 -> mt ()
+                  | _ -> pr_arg (pr_or_var int) n
+              in
+              hov 1 (
+                keyword "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
+              keyword "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
             | TacSolve tl ->
-              str "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
+              keyword "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
+              keyword "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(_,Tacexp e) ->
+              pr.pr_tactic (latom,E) e, latom
             | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
-              str "constr:" ++ pr.pr_constr c, latom
+              keyword "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(_,TacFreshId l) ->
+              keyword "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)),
+              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
+            | 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"
+            pr_with_comments loc (
+              str "<" ++ keyword "dynamic" ++ str (" [" ^ (Dyn.tag t)^"]>")
+            )
+          | MetaIdArg (loc,true,s) ->
+            pr_with_comments loc (str ("$" ^ s))
+          | MetaIdArg (loc,false,s) ->
+            pr_with_comments loc (keyword "constr:" ++ str(" $" ^ 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 ->
+            keyword "uconstr:" ++ pr.pr_uconstr c
+          | TacFreshId l ->
+            keyword "fresh" ++ pr_fresh_ids l
+          | TacPretype c ->
+            keyword "type_term" ++ pr.pr_constr c
+          | TacNumgoals ->
+            keyword "numgoals"
           | (TacCall _|Tacexp _ | TacGeneric _) as a ->
-            str "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
+            keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
 
         in pr_tac
 
@@ -1045,7 +1197,10 @@ struct
       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
+    make_pr_tac
+      pr raw_printers
+      tag_raw_atomic_tactic_expr tag_raw_tactic_expr
+      n t
 
   let pr_raw_tactic = pr_raw_tactic_level ltop
 
@@ -1077,13 +1232,15 @@ struct
           (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
+      make_pr_tac
+        pr glob_printers
+        tag_glob_atomic_tactic_expr tag_glob_tactic_expr
+        n t
     in
     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
@@ -1118,7 +1275,10 @@ struct
           (pr_glob_tactic_level env) pr_constr_pattern;
       }
       in
-      make_pr_tac pr typed_printers n t
+      make_pr_tac
+        pr typed_printers
+        tag_atomic_tactic_expr tag_tactic_expr
+        n t
     in
     prtac n t
 
@@ -1126,7 +1286,16 @@ struct
 
 end
 
-include Make (Ppconstr)
+include Make (Ppconstr) (struct
+    let do_not_tag _ x = x
+    let tag_keyword                 = do_not_tag ()
+    let tag_glob_tactic_expr        = do_not_tag
+    let tag_glob_atomic_tactic_expr = do_not_tag
+    let tag_raw_tactic_expr         = do_not_tag
+    let tag_raw_atomic_tactic_expr  = do_not_tag
+    let tag_tactic_expr             = do_not_tag
+    let tag_atomic_tactic_expr      = do_not_tag
+end)
 
 (** Registering *)
 
@@ -1169,3 +1338,21 @@ let _ = Hook.set Tactic_debug.match_rule_printer
   (fun rl ->
     pr_match_rule false (pr_glob_tactic (Global.env()))
       (fun (_,p) -> pr_constr_pattern p) rl)
+
+module RichPp (Indexer : sig
+  val index : Ppannotation.t -> string
+end) = struct
+
+  include Make (Ppconstr.RichPp (Indexer)) (struct
+    open Ppannotation
+    open Indexer
+    let tag_keyword       = Pp.tag (Indexer.index AKeyword)
+    let tag_glob_tactic_expr        e = Pp.tag (index (AGlobTacticExpr e))
+    let tag_glob_atomic_tactic_expr a = Pp.tag (index (AGlobAtomicTacticExpr a))
+    let tag_raw_tactic_expr         e = Pp.tag (index (ARawTacticExpr e))
+    let tag_raw_atomic_tactic_expr  a = Pp.tag (index (ARawAtomicTacticExpr a))
+    let tag_tactic_expr             e = Pp.tag (index (ATacticExpr e))
+    let tag_atomic_tactic_expr      a = Pp.tag (index (AAtomicTacticExpr a))
+  end)
+
+end
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 1afd731b7..36d116f1a 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -6,4 +6,64 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** This module implements pretty-printers for tactic_expr syntactic
+    objects and their subcomponents. *)
+
+open Pp
+open Genarg
+open Names
+open Constrexpr
+open Tacexpr
+open Ppextend
+open Environ
+open Pattern
+open Misctypes
+
+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 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 extra_genarg_printer =
+    (Term.constr -> std_ppcmds) ->
+    (Term.constr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    'a -> std_ppcmds
+
+val declare_extra_genarg_pprule :
+  ('a, 'b, 'c) genarg_type ->
+  'a raw_extra_genarg_printer ->
+  'b glob_extra_genarg_printer ->
+  'c extra_genarg_printer -> unit
+
+type grammar_terminals = string option list
+
+type pp_tactic = {
+  pptac_args : argument_type list;
+  pptac_prods : int * grammar_terminals;
+}
+
+val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit
+val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
+
+(** The default pretty-printers produce {!Pp.std_ppcmds} that are
+    interpreted as raw strings. *)
 include Pptacticsig.Pp
+
+(** The rich pretty-printers produce {!Pp.std_ppcmds} that are
+    interpreted as annotated strings. The annotations can be
+    retrieved using {!RichPp.rich_pp}. Their definitions are
+    located in {!Ppannotation.t}.
+
+    Please refer to {!RichPp} to know what are the requirements over
+    [Indexer.index] behavior. *)
+module RichPp (Indexer : sig val index : Ppannotation.t -> string end)
+  : Pptacticsig.Pp
+
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index f088d7b74..355055e6d 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -22,40 +22,6 @@ module type Pp = sig
   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
 
-  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 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 extra_genarg_printer =
-      (Term.constr -> std_ppcmds) ->
-      (Term.constr -> std_ppcmds) ->
-      (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-      'a -> std_ppcmds
-
-  val declare_extra_genarg_pprule :
-    ('a, 'b, 'c) genarg_type ->
-    'a raw_extra_genarg_printer ->
-    'b glob_extra_genarg_printer ->
-    'c extra_genarg_printer -> unit
-
-  type grammar_terminals = string option list
-
-  type pp_tactic = {
-    pptac_args : argument_type list;
-    pptac_prods : int * grammar_terminals;
-  }
-
-  val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit
-  val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
-
   val pr_clauses :  bool option ->
     ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
   val pr_raw_generic :
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 315301d93..70c0163bf 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -14,7 +14,6 @@ open Util
 open Extend
 open Vernacexpr
 open Pputils
-open Pptactic
 open Libnames
 open Constrexpr
 open Constrexpr_ops
@@ -22,6 +21,7 @@ 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,6 +30,7 @@ module Make
 
   open Taggers
   open Ppconstr
+  open Pptactic
 
   let keyword s = tag_keyword (str s)
 
@@ -1263,7 +1264,7 @@ module Make
 
 end
 
-include Make (Ppconstr) (struct
+include Make (Ppconstr) (Pptactic) (struct
   let do_not_tag _ x = x
   let tag_keyword = do_not_tag ()
   let tag_vernac  = do_not_tag
@@ -1273,10 +1274,13 @@ module RichPp (Indexer : sig
   val index : Ppannotation.t -> string
 end) = struct
 
-  include Make (Ppconstr.RichPp (Indexer)) (struct
-    open Ppannotation
-    let tag_keyword  = Pp.tag (Indexer.index AKeyword)
-    let tag_vernac v = Pp.tag (Indexer.index (AVernac v))
-  end)
+  include Make
+    (Ppconstr.RichPp (Indexer))
+    (Pptactic.RichPp (Indexer))
+    (struct
+      open Ppannotation
+      let tag_keyword  = Pp.tag (Indexer.index AKeyword)
+      let tag_vernac v = Pp.tag (Indexer.index (AVernac v))
+     end)
 
 end
diff --git a/printing/richPrinter.ml b/printing/richPrinter.ml
index 07e97668c..66732319c 100644
--- a/printing/richPrinter.ml
+++ b/printing/richPrinter.ml
@@ -4,15 +4,16 @@ module Indexer = Indexer (struct type t = Ppannotation.t end)
 
 module RichPpConstr = Ppconstr.RichPp (Indexer)
 module RichPpVernac = Ppvernac.RichPp (Indexer)
+module RichPpTactic = Pptactic.RichPp (Indexer)
 
 type rich_pp =
     string
     * Ppannotation.t RichPp.located Xml_datatype.gxml
     * Xml_datatype.xml
 
-let richpp_vernac phrase_ast =
+let make_richpp pr ast =
   let raw_pp, rich_pp =
-    rich_pp Indexer.get_annotations (fun () -> RichPpVernac.pr_vernac phrase_ast)
+    rich_pp Indexer.get_annotations (fun () -> pr ast)
   in
   let xml = Ppannotation.(
     xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp
@@ -20,3 +21,6 @@ let richpp_vernac phrase_ast =
   in
   (raw_pp, rich_pp, xml)
 
+let richpp_vernac = make_richpp RichPpVernac.pr_vernac
+let richpp_constr = make_richpp RichPpConstr.pr_constr_expr
+let richpp_tactic env = make_richpp (RichPpTactic.pr_tactic env)
diff --git a/printing/richPrinter.mli b/printing/richPrinter.mli
index 60d002596..9d02ad294 100644
--- a/printing/richPrinter.mli
+++ b/printing/richPrinter.mli
@@ -33,3 +33,9 @@ type rich_pp =
 
 (** [richpp_vernac phrase] produces a rich pretty-printing of [phrase]. *)
 val richpp_vernac : Vernacexpr.vernac_expr -> rich_pp
+
+(** [richpp_constr constr] produces a rich pretty-printing of [constr]. *)
+val richpp_constr : Constrexpr.constr_expr -> rich_pp
+
+(** [richpp_tactic constr] produces a rich pretty-printing of [tactic]. *)
+val richpp_tactic : Environ.env -> Tacexpr.tactic_expr -> rich_pp