Ppannotation.t: New constructor AVernac.

Ppvernac.RichPp: New rich pretty-printer.

3 files changed, 716 insertions, 494 deletions

diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
index 549a0dab8..3274a7bdc 100644
--- a/printing/ppannotation.ml
+++ b/printing/ppannotation.ml
@@ -6,9 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Constrexpr
 open Ppextend
+open Constrexpr
+open Vernacexpr
 
 type t =
   | AUnparsing  of unparsing
   | AConstrExpr of constr_expr
+  | AVernac     of vernac_expr
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
index 54f70aeda..a462c9f33 100644
--- a/printing/ppannotation.mli
+++ b/printing/ppannotation.mli
@@ -9,9 +9,11 @@
 (** This module defines the annotations that are attached to
     semi-structured pretty-printing of Coq syntactic objects. *)
 
-open Constrexpr
 open Ppextend
+open Constrexpr
+open Vernacexpr
 
 type t =
   | AUnparsing  of unparsing
   | AConstrExpr of constr_expr
+  | AVernac     of vernac_expr
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 67e11bb09..ecbc4a20e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -20,7 +20,12 @@ open Constrexpr
 open Constrexpr_ops
 open Decl_kinds
 
-module Make (Ppconstr : Ppconstrsig.Pp) = struct
+module Make
+  (Ppconstr : Ppconstrsig.Pp)
+  (Tagger   : sig
+    val tag_vernac : vernac_expr -> std_ppcmds -> std_ppcmds
+  end)
+= struct
 
   open Ppconstr
 
@@ -449,8 +454,8 @@ module Make (Ppconstr : Ppconstrsig.Pp) = struct
       | PrintVisibility s -> str "Print Visibility" ++ pr_opt str s
       | PrintAbout qid -> str "About" ++ spc()  ++ pr_smart_global qid
       | PrintImplicit qid -> str "Print Implicit" ++ spc()  ++ pr_smart_global qid
-(* spiwack: command printing all the axioms and section variables used in a
-   term *)
+      (* spiwack: command printing all the axioms and section variables used in a
+         term *)
       | PrintAssumptions (b, t, qid) ->
         let cmd = match b, t with
           | true, true -> "Print All Dependencies"
@@ -466,315 +471,431 @@ module Make (Ppconstr : Ppconstrsig.Pp) = struct
 
     let pr_using e = str (Proof_using.to_string e) in
 
-    let rec pr_vernac = function
-      | VernacPolymorphic (poly, v) ->
-        let s = if poly then str"Polymorphic" else str"Monomorphic" in
-        s ++ pr_vernac v
-      | VernacProgram v -> str"Program" ++ spc() ++ pr_vernac v
-      | VernacLocal (local, v) -> pr_locality local ++ spc() ++ pr_vernac v
-
-  (* Stm *)
-      | VernacStm JoinDocument -> str"Stm JoinDocument"
-      | VernacStm PrintDag -> str"Stm PrintDag"
-      | VernacStm Finish -> str"Stm Finish"
-      | VernacStm Wait -> str"Stm Wait"
-      | VernacStm (Observe id) ->
-        str"Stm Observe " ++ str(Stateid.to_string id)
-      | VernacStm (Command v) -> str"Stm Command " ++ pr_vernac v
-      | VernacStm (PGLast v) -> str"Stm PGLast " ++ pr_vernac v
-
-  (* Proof management *)
-      | VernacAbortAll -> str "Abort All"
-      | VernacRestart -> str"Restart"
-      | VernacUnfocus -> str"Unfocus"
-      | VernacUnfocused -> str"Unfocused"
-      | VernacGoal c -> str"Goal" ++ pr_lconstrarg c
-      | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
-      | VernacUndo i -> if Int.equal i 1 then str"Undo" else str"Undo" ++ pr_intarg i
-      | VernacUndoTo i -> str"Undo" ++ spc() ++ str"To" ++ pr_intarg i
-      | VernacBacktrack (i,j,k) ->
-        str "Backtrack" ++  spc() ++ prlist_with_sep sep int [i;j;k]
-      | VernacFocus i -> str"Focus" ++ pr_opt int i
-      | VernacShow s ->
-        let pr_goal_reference = function
-          | OpenSubgoals -> mt ()
-          | NthGoal n -> spc () ++ int n
-          | GoalId n -> spc () ++ str n in
-        let pr_showable = function
-          | ShowGoal n -> str"Show" ++ pr_goal_reference n
-          | ShowGoalImplicitly n -> str"Show Implicit Arguments" ++ pr_opt int n
-          | ShowProof -> str"Show Proof"
-          | ShowNode -> str"Show Node"
-          | ShowScript -> str"Show Script"
-          | ShowExistentials -> str"Show Existentials"
-          | ShowUniverses -> str"Show Universes"
-          | ShowTree -> str"Show Tree"
-          | ShowProofNames -> str"Show Conjectures"
-          | ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro")
-          | ShowMatch id -> str"Show Match " ++ pr_lident id
-          | ShowThesis -> str "Show Thesis"
-        in pr_showable s
-      | VernacCheckGuard -> str"Guarded"
-
-  (* Resetting *)
-      | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id
-      | VernacResetInitial -> str"Reset Initial"
-      | VernacBack i -> if Int.equal i 1 then str"Back" else str"Back" ++ pr_intarg i
-      | VernacBackTo i -> str"BackTo" ++ pr_intarg i
-
-  (* State management *)
-      | VernacWriteState s -> str"Write State" ++ spc () ++ qs s
-      | VernacRestoreState s -> str"Restore State" ++ spc() ++ qs s
-
-  (* Control *)
-      | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose"
-                                                    ++ spc()) else spc()  ++ qs s
-      | VernacTime v -> str"Time" ++ spc() ++ pr_vernac_list v
-      | VernacTimeout(n,v) -> str"Timeout " ++ int n ++ spc() ++ pr_vernac v
-      | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v
-      | VernacError _ -> str"No-parsing-rule for VernacError"
-
-  (* Syntax *)
-      | VernacTacticNotation (n,r,e) ->
-        pr_grammar_tactic_rule n ("",r,e)
-      | VernacOpenCloseScope (_,(opening,sc)) ->
-        str (if opening then "Open " else "Close ") ++
-          str "Scope" ++ spc() ++ str sc
-      | VernacDelimiters (sc,key) ->
-        str"Delimit Scope" ++ spc () ++ str sc ++
-          spc() ++ str "with " ++ str key
-      | VernacBindScope (sc,cll) ->
-        str"Bind Scope" ++ spc () ++ str sc ++
-          spc() ++ str "with " ++ prlist_with_sep spc pr_smart_global cll
-      | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function
-          | None -> str"_"
-          | Some sc -> str sc in
-                                        str"Arguments Scope" ++ spc() ++
-                                          pr_smart_global q
-                                        ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
-      | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *)
-        hov 0 (hov 0 (str"Infix "
-                      ++ qs s ++ str " :=" ++ pr_constrarg q) ++
-                 pr_syntax_modifiers mv ++
-                 (match sn with
-                   | None -> mt()
-                   | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
-      | VernacNotation (_,c,((_,s),l),opt) ->
-        let ps =
-          let n = String.length s in
-          if n > 2 && s.[0] == '\'' && s.[n-1] == '\''
-          then
-            let s' = String.sub s 1 (n-2) in
-            if String.contains s' '\'' then qs s else str s'
-          else qs s in
-        hov 2 (str"Notation" ++ spc() ++ ps ++
-                 str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
-                 (match opt with
-                   | None -> mt()
-                   | Some sc -> str" :" ++ spc() ++ str sc))
-      | VernacSyntaxExtension (_,(s,l)) ->
-        str"Reserved Notation" ++ spc() ++ pr_located qs s ++
-          pr_syntax_modifiers l
-      | VernacNotationAddFormat(s,k,v) ->
-        str"Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
-
-  (* Gallina *)
-      | VernacDefinition (d,id,b) -> (* A verifier... *)
-        let pr_def_token (l,dk) =
-          let l = match l with Some x -> x | None -> Decl_kinds.Global in
-          str (Kindops.string_of_definition_kind (l,false,dk)) in
-        let pr_reduce = function
-          | None -> mt()
-          | Some r ->
-            str"Eval" ++ spc() ++
-              pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++
-              str" in" ++ spc() in
-        let pr_def_body = function
-          | DefineBody (bl,red,body,d) ->
-            let ty = match d with
-              | None -> mt()
-              | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
-            in
-            (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
-          | ProveBody (bl,t) ->
-            (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in
-        let (binds,typ,c) = pr_def_body b in
-        hov 2 (pr_def_token d ++ spc() ++ pr_lident id ++ binds ++ typ ++
-                 (match c with
-                   | None -> mt()
-                   | Some cc -> str" :=" ++ spc() ++ cc))
-
-      | VernacStartTheoremProof (ki,l,_) ->
-        hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
-                 prlist (pr_statement (spc () ++ str "with")) (List.tl l))
-
-      | VernacEndProof Admitted -> str"Admitted"
-      | VernacEndProof (Proved (opac,o)) -> (match o with
-          | None -> if opac then str"Qed" else str"Defined"
-          | Some (id,th) -> (match th with
-              | None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_lident id
-              | Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id))
-      | VernacExactProof c ->
-        hov 2 (str"Proof" ++ pr_lconstrarg c)
-      | VernacAssumption (stre,_,l) ->
-        let n = List.length (List.flatten (List.map fst (List.map snd l))) in
-        hov 2
-          (pr_assumption_token (n > 1) stre ++ spc() ++
-             pr_ne_params_list pr_lconstr_expr l)
-      | VernacInductive (p,f,l) ->
-        let pr_constructor (coe,(id,c)) =
-          hov 2 (pr_lident id ++ str" " ++
-                   (if coe then str":>" else str":") ++
-                   pr_spc_lconstr c) in
-        let pr_constructor_list b l = match l with
-          | Constructors [] -> mt()
-          | Constructors l ->
-            let fst_sep = match l with [_] -> "   " | _ -> " | " in
-            pr_com_at (begin_of_inductive l) ++
-              fnl() ++ str fst_sep ++
-              prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
-          | RecordDecl (c,fs) ->
-            pr_record_decl b c fs in
-        let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
-          hov 0 (
-            str key ++ spc() ++
-              (if coe then str"> " else str"") ++ pr_lident id ++
-              pr_and_type_binders_arg indpar ++ spc() ++
-              Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
-              str" :=") ++ pr_constructor_list k lc ++
-            prlist (pr_decl_notation pr_constr) ntn
-        in
-        let key =
-          let (_,_,_,k,_),_ = List.hd l in
-          match k with Record -> "Record" | Structure -> "Structure"
-            | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
-            | Class _ -> "Class" | Variant -> "Variant" in
-        hov 1 (pr_oneind key (List.hd l)) ++
-          (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
-
-
-      | VernacFixpoint (local, recs) ->
-        let local = match local with
-          | Some Discharge -> "Let "
-          | Some Local -> "Local "
-          | None | Some Global -> ""
-        in
-        let pr_onerec = function
-          | ((loc,id),ro,bl,type_,def),ntn ->
-            let annot = pr_guard_annot pr_lconstr_expr bl ro in
-            pr_id id ++ pr_binders_arg bl ++ annot
-            ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
-            ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
+    let rec pr_vernac v =
+      let return = Tagger.tag_vernac v in
+      match v with
+        | VernacPolymorphic (poly, v) ->
+          let s = if poly then str"Polymorphic" else str"Monomorphic" in
+          return (s ++ pr_vernac v)
+        | VernacProgram v ->
+          return (str"Program" ++ spc() ++ pr_vernac v)
+        | VernacLocal (local, v) ->
+          return (pr_locality local ++ spc() ++ pr_vernac v)
+
+        (* Stm *)
+        | VernacStm JoinDocument ->
+          return (str"Stm JoinDocument")
+        | VernacStm PrintDag ->
+          return (str"Stm PrintDag")
+        | VernacStm Finish ->
+          return (str"Stm Finish")
+        | VernacStm Wait ->
+          return (str"Stm Wait")
+        | VernacStm (Observe id) ->
+          return (str"Stm Observe " ++ str(Stateid.to_string id))
+        | VernacStm (Command v) ->
+          return (str"Stm Command " ++ pr_vernac v)
+        | VernacStm (PGLast v) ->
+          return (str"Stm PGLast " ++ pr_vernac v)
+
+        (* Proof management *)
+        | VernacAbortAll ->
+          return (str "Abort All")
+        | VernacRestart ->
+          return (str"Restart")
+        | VernacUnfocus ->
+          return (str"Unfocus")
+        | VernacUnfocused ->
+          return (str"Unfocused")
+        | VernacGoal c ->
+          return (str"Goal" ++ pr_lconstrarg c)
+        | VernacAbort id ->
+          return (str"Abort" ++ pr_opt pr_lident id)
+        | VernacUndo i ->
+          return (
+            if Int.equal i 1 then str"Undo" else str"Undo" ++ pr_intarg i
+          )
+        | VernacUndoTo i ->
+          return (str"Undo" ++ spc() ++ str"To" ++ pr_intarg i)
+        | VernacBacktrack (i,j,k) ->
+          return (str "Backtrack" ++  spc() ++ prlist_with_sep sep int [i;j;k])
+        | VernacFocus i ->
+          return (str"Focus" ++ pr_opt int i)
+        | VernacShow s ->
+          let pr_goal_reference = function
+            | OpenSubgoals -> mt ()
+            | NthGoal n -> spc () ++ int n
+            | GoalId n -> spc () ++ str n in
+          let pr_showable = function
+            | ShowGoal n -> str"Show" ++ pr_goal_reference n
+            | ShowGoalImplicitly n -> str"Show Implicit Arguments" ++ pr_opt int n
+            | ShowProof -> str"Show Proof"
+            | ShowNode -> str"Show Node"
+            | ShowScript -> str"Show Script"
+            | ShowExistentials -> str"Show Existentials"
+            | ShowUniverses -> str"Show Universes"
+            | ShowTree -> str"Show Tree"
+            | ShowProofNames -> str"Show Conjectures"
+            | ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro")
+            | ShowMatch id -> str"Show Match " ++ pr_lident id
+            | ShowThesis -> str "Show Thesis"
+          in
+          return (pr_showable s)
+        | VernacCheckGuard ->
+          return (str"Guarded")
+
+      (* Resetting *)
+        | VernacResetName id ->
+          return (str"Reset" ++ spc() ++ pr_lident id)
+        | VernacResetInitial ->
+          return (str"Reset Initial")
+        | VernacBack i ->
+          return (
+            if Int.equal i 1 then str"Back" else str"Back" ++ pr_intarg i
+          )
+        | VernacBackTo i ->
+          return (str"BackTo" ++ pr_intarg i)
+
+      (* State management *)
+        | VernacWriteState s ->
+          return (str"Write State" ++ spc () ++ qs s)
+        | VernacRestoreState s ->
+          return  (str"Restore State" ++ spc() ++ qs s)
+
+      (* Control *)
+        | VernacLoad (f,s) ->
+          return (
+            str"Load"
+            ++ if f then
+                (spc() ++ str"Verbose" ++ spc())
+              else
+                spc() ++ qs s
+          )
+        | VernacTime v ->
+          return (str"Time" ++ spc() ++ pr_vernac_list v)
+        | VernacTimeout(n,v) ->
+          return (str"Timeout " ++ int n ++ spc() ++ pr_vernac v)
+        | VernacFail v ->
+          return (str"Fail" ++ spc() ++ pr_vernac v)
+        | VernacError _ ->
+          return (str"No-parsing-rule for VernacError")
+
+      (* Syntax *)
+        | VernacTacticNotation (n,r,e) ->
+          return (pr_grammar_tactic_rule n ("",r,e))
+        | VernacOpenCloseScope (_,(opening,sc)) ->
+          return (
+            str (if opening then "Open " else "Close ") ++
+              str "Scope" ++ spc() ++ str sc
+          )
+        | VernacDelimiters (sc,key) ->
+          return (
+            str"Delimit Scope" ++ spc () ++ str sc ++
+              spc() ++ str "with " ++ str key
+          )
+        | VernacBindScope (sc,cll) ->
+          return (
+            str"Bind Scope" ++ spc () ++ str sc ++
+              spc() ++ str "with " ++ prlist_with_sep spc pr_smart_global cll
+          )
+        | VernacArgumentsScope (q,scl) ->
+          let pr_opt_scope = function
+            | None -> str"_"
+            | Some sc -> str sc
+          in
+          return (
+            str"Arguments Scope"
+            ++ spc() ++ pr_smart_global q
+            ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
+          )
+        | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *)
+          return (
+            hov 0 (hov 0 (str"Infix "
+                          ++ qs s ++ str " :=" ++ pr_constrarg q) ++
+                     pr_syntax_modifiers mv ++
+                     (match sn with
+                       | None -> mt()
+                       | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
+          )
+        | VernacNotation (_,c,((_,s),l),opt) ->
+          let ps =
+            let n = String.length s in
+            if n > 2 && s.[0] == '\'' && s.[n-1] == '\''
+            then
+              let s' = String.sub s 1 (n-2) in
+              if String.contains s' '\'' then qs s else str s'
+            else qs s
+          in
+          return (
+            hov 2 (str"Notation" ++ spc() ++ ps ++
+                     str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
+                     (match opt with
+                       | None -> mt()
+                       | Some sc -> str" :" ++ spc() ++ str sc))
+          )
+        | VernacSyntaxExtension (_,(s,l)) ->
+          return (
+            str"Reserved Notation" ++ spc() ++ pr_located qs s ++
+              pr_syntax_modifiers l
+          )
+        | VernacNotationAddFormat(s,k,v) ->
+          return (
+            str"Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
+          )
+
+        (* Gallina *)
+        | VernacDefinition (d,id,b) -> (* A verifier... *)
+          let pr_def_token (l,dk) =
+            let l = match l with Some x -> x | None -> Decl_kinds.Global in
+            str (Kindops.string_of_definition_kind (l,false,dk))
+          in
+          let pr_reduce = function
+            | None -> mt()
+            | Some r ->
+              str"Eval" ++ spc() ++
+                pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++
+                str" in" ++ spc()
+          in
+          let pr_def_body = function
+            | DefineBody (bl,red,body,d) ->
+              let ty = match d with
+                | None -> mt()
+                | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
+              in
+              (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
+            | ProveBody (bl,t) ->
+              (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in
+          let (binds,typ,c) = pr_def_body b in
+          return (
+            hov 2 (pr_def_token d ++ spc() ++ pr_lident id ++ binds ++ typ ++
+                     (match c with
+                       | None -> mt()
+                       | Some cc -> str" :=" ++ spc() ++ cc))
+          )
+
+        | VernacStartTheoremProof (ki,l,_) ->
+          return (
+            hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
+                     prlist (pr_statement (spc () ++ str "with")) (List.tl l))
+          )
+
+        | VernacEndProof Admitted ->
+          return (str"Admitted")
+
+        | VernacEndProof (Proved (opac,o)) -> return (
+          match o with
+            | None -> if opac then str"Qed" else str"Defined"
+            | Some (id,th) -> (match th with
+                | None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_lident id
+                | Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)
+        )
+        | VernacExactProof c ->
+          return (hov 2 (str"Proof" ++ pr_lconstrarg c))
+        | VernacAssumption (stre,_,l) ->
+          let n = List.length (List.flatten (List.map fst (List.map snd l))) in
+          return (
+            hov 2
+              (pr_assumption_token (n > 1) stre ++ spc() ++
+                 pr_ne_params_list pr_lconstr_expr l)
+          )
+        | VernacInductive (p,f,l) ->
+          let pr_constructor (coe,(id,c)) =
+            hov 2 (pr_lident id ++ str" " ++
+                     (if coe then str":>" else str":") ++
+                     pr_spc_lconstr c)
+          in
+          let pr_constructor_list b l = match l with
+            | Constructors [] -> mt()
+            | Constructors l ->
+              let fst_sep = match l with [_] -> "   " | _ -> " | " in
+              pr_com_at (begin_of_inductive l) ++
+                fnl() ++ str fst_sep ++
+                prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
+            | RecordDecl (c,fs) ->
+              pr_record_decl b c fs
+          in
+          let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
+            hov 0 (
+              str key ++ spc() ++
+                (if coe then str"> " else str"") ++ pr_lident id ++
+                pr_and_type_binders_arg indpar ++ spc() ++
+                Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
+                str" :=") ++ pr_constructor_list k lc ++
               prlist (pr_decl_notation pr_constr) ntn
-        in
-        hov 0 (str local ++ str "Fixpoint" ++ spc() ++
-                 prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)
-
-      | VernacCoFixpoint (local, corecs) ->
-        let local = match local with
-          | Some Discharge -> "Let "
-          | Some Local -> "Local "
-          | None | Some Global -> ""
-        in
-        let pr_onecorec (((loc,id),bl,c,def),ntn) =
-          pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
-            spc() ++ pr_lconstr_expr c ++
-            pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
-            prlist (pr_decl_notation pr_constr) ntn
-        in
-        hov 0 (str local ++ str "CoFixpoint" ++ spc() ++
-                 prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)
-      | VernacScheme l ->
-        hov 2 (str"Scheme" ++ spc() ++
-                 prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l)
-      | VernacCombinedScheme (id, l) ->
-        hov 2 (str"Combined Scheme" ++ spc() ++
-                 pr_lident id ++ spc() ++ str"from" ++ spc() ++
-                 prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
-      | VernacUniverse v ->
-        hov 2 (str"Universe" ++ spc () ++
-                 prlist_with_sep (fun _ -> str",") pr_lident v)
-      | VernacConstraint v ->
-        let pr_uconstraint (l, d, r) =
-          pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r
-        in
-        hov 2 (str"Constraint" ++ spc () ++
-                 prlist_with_sep (fun _ -> str",") pr_uconstraint v)
-
-  (* Gallina extensions *)
-      | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
-      | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id)
-      | VernacRequire (exp, l) -> hov 2
-        (str "Require" ++ spc() ++ pr_require_token exp ++
-           prlist_with_sep sep pr_module l)
-      | VernacImport (f,l) ->
-        (if f then str"Export" else str"Import") ++ spc() ++
-          prlist_with_sep sep pr_import_module l
-      | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_smart_global q
-      | VernacCoercion (_,id,c1,c2) ->
-        hov 1 (
-          str"Coercion" ++ spc() ++
-            pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
-            spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
-      | VernacIdentityCoercion (_,id,c1,c2) ->
-        hov 1 (
-          str"Identity Coercion" ++ spc() ++ pr_lident id ++
-            spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
-            spc() ++ pr_class_rawexpr c2)
-
-      | VernacInstance (abst, sup, (instid, bk, cl), props, pri) ->
-        hov 1 (
-          (if abst then str"Declare " else mt ()) ++
-            str"Instance" ++
-            (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
-                Anonymous -> mt ()) ++
-            pr_and_type_binders_arg sup ++
-            str":" ++ spc () ++
-            pr_constr cl ++ pr_priority pri ++
-            (match props with
-              | Some (_,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
-              | None -> mt()))
-
-      | VernacContext l ->
-        hov 1 (
-          str"Context" ++ spc () ++ pr_and_type_binders_arg l)
-
-
-      | VernacDeclareInstances (ids, pri) ->
-        hov 1 ( str"Existing" ++ spc () ++
-                  str(String.plural (List.length ids) "Instance") ++
-                  spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri)
-
-      | VernacDeclareClass id ->
-        hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id)
-
-  (* Modules and Module Types *)
-      | VernacDefineModule (export,m,bl,tys,bd) ->
-        let b = pr_module_binders bl pr_lconstr in
-        hov 2 (str"Module" ++ spc() ++ pr_require_token export ++
-                 pr_lident m ++ b ++
-                 pr_of_module_type pr_lconstr tys ++
-                 (if List.is_empty bd then mt () else str ":= ") ++
-                 prlist_with_sep (fun () -> str " <+ ")
-                 (pr_module_ast_inl true pr_lconstr) bd)
-      | VernacDeclareModule (export,id,bl,m1) ->
-        let b = pr_module_binders bl pr_lconstr in
-        hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++
-                 pr_lident id ++ b ++
-                 pr_module_ast_inl true pr_lconstr m1)
-      | VernacDeclareModuleType (id,bl,tyl,m) ->
-        let b = pr_module_binders bl pr_lconstr in
-        let pr_mt = pr_module_ast_inl true pr_lconstr in
-        hov 2 (str"Module Type " ++ pr_lident id ++ b ++
-                 prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++
-                 (if List.is_empty m then mt () else str ":= ") ++
-                 prlist_with_sep (fun () -> str " <+ ") pr_mt m)
-      | VernacInclude (mexprs) ->
-        let pr_m = pr_module_ast_inl false pr_lconstr in
-        hov 2 (str"Include" ++ spc() ++
-                 prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
-
-      (* Solving *)
+          in
+          let key =
+            let (_,_,_,k,_),_ = List.hd l in
+            match k with Record -> "Record" | Structure -> "Structure"
+              | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+              | Class _ -> "Class" | Variant -> "Variant"
+          in
+          return (
+            hov 1 (pr_oneind key (List.hd l)) ++
+              (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
+          )
+
+        | VernacFixpoint (local, recs) ->
+          let local = match local with
+            | Some Discharge -> "Let "
+            | Some Local -> "Local "
+            | None | Some Global -> ""
+          in
+          let pr_onerec = function
+            | ((loc,id),ro,bl,type_,def),ntn ->
+              let annot = pr_guard_annot pr_lconstr_expr bl ro in
+              pr_id id ++ pr_binders_arg bl ++ annot
+              ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
+              ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
+                prlist (pr_decl_notation pr_constr) ntn
+          in
+          return (
+            hov 0 (str local ++ str "Fixpoint" ++ spc() ++
+                     prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)
+          )
+
+        | VernacCoFixpoint (local, corecs) ->
+          let local = match local with
+            | Some Discharge -> "Let "
+            | Some Local -> "Local "
+            | None | Some Global -> ""
+          in
+          let pr_onecorec (((loc,id),bl,c,def),ntn) =
+            pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+              spc() ++ pr_lconstr_expr c ++
+              pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
+              prlist (pr_decl_notation pr_constr) ntn
+          in
+          return (
+            hov 0 (str local ++ str "CoFixpoint" ++ spc() ++
+                     prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)
+          )
+        | VernacScheme l ->
+          return (
+            hov 2 (str"Scheme" ++ spc() ++
+                     prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l)
+          )
+        | VernacCombinedScheme (id, l) ->
+          return (
+            hov 2 (str"Combined Scheme" ++ spc() ++
+                     pr_lident id ++ spc() ++ str"from" ++ spc() ++
+                     prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
+          )
+        | VernacUniverse v ->
+          return (
+            hov 2 (str"Universe" ++ spc () ++
+                     prlist_with_sep (fun _ -> str",") pr_lident v)
+          )
+        | VernacConstraint v ->
+          let pr_uconstraint (l, d, r) =
+            pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r
+          in
+          return (
+            hov 2 (str"Constraint" ++ spc () ++
+                     prlist_with_sep (fun _ -> str",") pr_uconstraint v)
+          )
+
+        (* Gallina extensions *)
+        | VernacBeginSection id ->
+          return (hov 2 (str"Section" ++ spc () ++ pr_lident id))
+        | VernacEndSegment id ->
+          return (hov 2 (str"End" ++ spc() ++ pr_lident id))
+        | VernacRequire (exp, l) ->
+          return (
+            hov 2
+              (str "Require" ++ spc() ++ pr_require_token exp ++
+                 prlist_with_sep sep pr_module l)
+          )
+        | VernacImport (f,l) ->
+          return (
+            (if f then str"Export" else str"Import") ++ spc() ++
+              prlist_with_sep sep pr_import_module l
+          )
+        | VernacCanonical q ->
+          return (
+            str"Canonical Structure" ++ spc() ++ pr_smart_global q
+          )
+        | VernacCoercion (_,id,c1,c2) ->
+          return (
+            hov 1 (
+              str"Coercion" ++ spc() ++
+                pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
+                spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
+          )
+        | VernacIdentityCoercion (_,id,c1,c2) ->
+          return (
+            hov 1 (
+              str"Identity Coercion" ++ spc() ++ pr_lident id ++
+                spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
+                spc() ++ pr_class_rawexpr c2)
+          )
+
+        | VernacInstance (abst, sup, (instid, bk, cl), props, pri) ->
+          return (
+            hov 1 (
+              (if abst then str"Declare " else mt ()) ++
+                str"Instance" ++
+                (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
+                    Anonymous -> mt ()) ++
+                pr_and_type_binders_arg sup ++
+                str":" ++ spc () ++
+                pr_constr cl ++ pr_priority pri ++
+                (match props with
+                  | Some (_,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
+                  | None -> mt()))
+          )
+
+        | VernacContext l ->
+          return (
+            hov 1 (
+              str"Context" ++ spc () ++ pr_and_type_binders_arg l)
+          )
+
+        | VernacDeclareInstances (ids, pri) ->
+          return (
+            hov 1 (str"Existing" ++ spc () ++
+                     str(String.plural (List.length ids) "Instance") ++
+                     spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri)
+          )
+
+        | VernacDeclareClass id ->
+          return (
+            hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id)
+          )
+
+      (* Modules and Module Types *)
+        | VernacDefineModule (export,m,bl,tys,bd) ->
+          let b = pr_module_binders bl pr_lconstr in
+          return (
+            hov 2 (str"Module" ++ spc() ++ pr_require_token export ++
+                     pr_lident m ++ b ++
+                     pr_of_module_type pr_lconstr tys ++
+                     (if List.is_empty bd then mt () else str ":= ") ++
+                     prlist_with_sep (fun () -> str " <+ ")
+                     (pr_module_ast_inl true pr_lconstr) bd)
+          )
+        | VernacDeclareModule (export,id,bl,m1) ->
+          let b = pr_module_binders bl pr_lconstr in
+          return (
+            hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++
+                     pr_lident id ++ b ++
+                     pr_module_ast_inl true pr_lconstr m1)
+          )
+        | VernacDeclareModuleType (id,bl,tyl,m) ->
+          let b = pr_module_binders bl pr_lconstr in
+          let pr_mt = pr_module_ast_inl true pr_lconstr in
+          return (
+            hov 2 (str"Module Type " ++ pr_lident id ++ b ++
+                     prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++
+                     (if List.is_empty m then mt () else str ":= ") ++
+                     prlist_with_sep (fun () -> str " <+ ") pr_mt m)
+          )
+        | VernacInclude (mexprs) ->
+          let pr_m = pr_module_ast_inl false pr_lconstr in
+          return (
+            hov 2 (str"Include" ++ spc() ++
+                     prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
+          )
+        (* Solving *)
       | VernacSolve (i,info,tac,deftac) ->
         let pr_goal_selector = function
           | SelectNth i -> int i ++ str":"
@@ -787,188 +908,268 @@ module Make (Ppconstr : Ppconstrsig.Pp) = struct
             | None -> mt ()
             | Some i -> str"Info"++spc()++int i++spc()
         in
-        (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++
+        return (
+          (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++
           pr_info ++
           pr_raw_tactic tac
-        ++ (if deftac then str ".." else mt ())
-      | VernacSolveExistential (i,c) ->
-        str"Existential " ++ int i ++ pr_lconstrarg c
-
-      (* Auxiliary file and library management *)
-      | VernacAddLoadPath (fl,s,d) -> hov 2
-        (str"Add" ++
-           (if fl then str" Rec " else spc()) ++
-           str"LoadPath" ++ spc() ++ qs s ++
-           (match d with
-             | None -> mt()
-             | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir))
-      | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s
-      | VernacAddMLPath (fl,s) ->
-        str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s
-      | VernacDeclareMLModule (l) ->
-        hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
-      | VernacChdir s -> str"Cd" ++ pr_opt qs s
-
-  (* Commands *)
-      | VernacDeclareTacticDefinition (rc,l) ->
-        let pr_tac_body (id, redef, body) =
-          let idl, body =
-            match body with
-              | Tacexpr.TacFun (idl,b) -> idl,b
-              | _ -> [], body in
-          pr_ltac_ref id ++
-            prlist (function None -> str " _"
-              | Some id -> spc () ++ pr_id id) idl
-          ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
-            pr_raw_tactic body
-        in
-        hov 1
-          (str "Ltac " ++
-             prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
-      | VernacCreateHintDb (dbname,b) ->
-        hov 1 (str "Create HintDb " ++
-                 str dbname ++ (if b then str" discriminated" else mt ()))
-      | VernacRemoveHints (dbnames, ids) ->
-        hov 1 (str "Remove Hints " ++
-                 prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
-                 pr_opt_hintbases dbnames)
-      | VernacHints (_, dbnames,h) ->
-        pr_hints dbnames h pr_constr pr_constr_pattern_expr
-      | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) ->
-        hov 2
-          (str"Notation " ++ pr_lident id ++ spc () ++
-             prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
-             pr_syntax_modifiers
-             (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v]))
-      | VernacDeclareImplicits (q,[]) ->
-        hov 2 (str"Implicit Arguments" ++ spc() ++ pr_smart_global q)
-      | VernacDeclareImplicits (q,impls) ->
-        hov 1 (str"Implicit Arguments " ++
-                 spc() ++ pr_smart_global q ++ spc() ++
-                 prlist_with_sep spc (fun imps ->
-                   str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
-                 impls)
-      | VernacArguments (q, impl, nargs, mods) ->
-        hov 2 (str"Arguments" ++ spc() ++
-                 pr_smart_global q ++
-                 let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
-                 let pr_if b x = if b then x else str "" in
-                 let pr_br imp max x = match imp, max with
-                   | true, false -> str "[" ++ x ++ str "]"
-                   | true, true -> str "{" ++ x ++ str "}"
-                   | _ -> x in
-                 let rec aux n l =
-                   match n, l with
-                     | 0, l -> spc () ++ str"/" ++ aux ~-1 l
-                     | _, [] -> mt()
-                     | n, (id,k,s,imp,max) :: tl ->
-                       spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
-                         aux (n-1) tl in
-                 prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
-                   if not (List.is_empty mods) then str" : " else str"" ++
-                     prlist_with_sep (fun () -> str", " ++ spc()) (function
-                       | `ReductionDontExposeCase -> str "simpl nomatch"
-                       | `ReductionNeverUnfold -> str "simpl never"
-                       | `DefaultImplicits -> str "default implicits"
-                       | `Rename -> str "rename"
-                       | `Assert -> str "assert"
-                       | `ExtraScopes -> str "extra scopes"
-                       | `ClearImplicits -> str "clear implicits"
-                       | `ClearScopes -> str "clear scopes")
-                     mods)
-      | VernacReserve bl ->
-        let n = List.length (List.flatten (List.map fst bl)) in
-        hov 2 (str"Implicit Type" ++
-                 str (if n > 1 then "s " else " ") ++
-                 pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
-      | VernacGeneralizable g ->
-        hov 1 (str"Generalizable Variable" ++
-                 match g with
-                   | None -> str "s none"
-                   | Some [] -> str "s all"
-                   | Some idl ->
-                     str (if List.length idl > 1 then "s " else " ") ++
-                       prlist_with_sep spc pr_lident idl)
-      | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k ->
-        hov 1 (str "Transparent" ++
-                 spc() ++ prlist_with_sep sep pr_smart_global l)
-      | VernacSetOpacity(Conv_oracle.Opaque,l) ->
-        hov 1 (str "Opaque" ++
-                 spc() ++ prlist_with_sep sep pr_smart_global l)
-      | VernacSetOpacity _ ->
-        Errors.anomaly (str "VernacSetOpacity used to set something else")
-      | VernacSetStrategy l ->
-        let pr_lev = function
-        Conv_oracle.Opaque -> str"opaque"
-          | Conv_oracle.Expand -> str"expand"
-          | l when Conv_oracle.is_transparent l -> str"transparent"
-          | Conv_oracle.Level n -> int n in
-        let pr_line (l,q) =
-          hov 2 (pr_lev l ++ spc() ++
-                   str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") in
-        hov 1 (str "Strategy" ++ spc() ++
-                 hv 0 (prlist_with_sep sep pr_line l))
-      | VernacUnsetOption (na) ->
-        hov 1 (str"Unset" ++ spc() ++ pr_printoption na None)
-      | VernacSetOption (na,v) ->
-        hov 2 (str"Set" ++ spc() ++ pr_set_option na v)
-      | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l))
-      | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l))
-      | VernacMemOption (na,l) -> hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l))
-      | VernacPrintOption na -> hov 2 (str"Test" ++ spc() ++ pr_printoption na None)
-      | VernacCheckMayEval (r,io,c) ->
-        let pr_mayeval r c = match r with
-          | Some r0 ->
-            hov 2 (str"Eval" ++ spc() ++
-                     pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++
-                     spc() ++ str"in" ++ spc () ++ pr_lconstr c)
-          | None -> hov 2 (str"Check" ++ spc() ++ pr_lconstr c)
-        in
-        let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in
-        pr_i ++ pr_mayeval r c
-      | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c)
-      | VernacDeclareReduction (s,r) ->
-        str "Declare Reduction " ++ str s ++ str " := " ++
-          pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r
-      | VernacPrint p -> pr_printable p
-      | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
-      | VernacLocate loc ->
-        let pr_locate =function
-          | LocateAny qid -> pr_smart_global qid
-          | LocateTerm qid -> str "Term" ++ spc() ++ pr_smart_global qid
-          | LocateFile f -> str"File" ++ spc() ++ qs f
-          | LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid
-          | LocateModule qid -> str"Module" ++ spc () ++ pr_module qid
-          | LocateTactic qid -> str"Ltac" ++ spc () ++ pr_ltac_ref qid
-        in str"Locate" ++ spc() ++ pr_locate loc
-      | VernacRegister (id, RegisterInline) ->
-        hov 2
-          (str "Register Inline" ++ spc() ++ pr_lident id)
-      | VernacComments l ->
-        hov 2
-          (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l)
-      | VernacNop -> mt()
-
-  (* Toplevel control *)
-      | VernacToplevelControl exn -> pr_topcmd exn
-
-  (* For extension *)
-      | VernacExtend (s,c) -> pr_extend s c
-      | VernacProof (None, None) -> str "Proof"
-      | VernacProof (None, Some e) -> str "Proof " ++ pr_using e
-      | VernacProof (Some te, None) -> str "Proof with" ++ spc() ++ pr_raw_tactic te
-      | VernacProof (Some te, Some e) ->
-        str "Proof " ++ pr_using e ++ spc() ++
-          str "with" ++ spc() ++pr_raw_tactic te
-      | VernacProofMode s -> str ("Proof Mode "^s)
-      | VernacBullet b -> begin match b with
-          | Dash n -> str (String.make n '-')
-          | Star n -> str (String.make n '*')
-          | Plus n -> str (String.make n '+')
-      end ++ spc()
-      | VernacSubproof None -> str "{"
-      | VernacSubproof (Some i) -> str "BeginSubproof " ++ int i
-      | VernacEndSubproof -> str "}"
+          ++ (if deftac then str ".." else mt ())
+        )
+        | VernacSolveExistential (i,c) ->
+          return (str"Existential " ++ int i ++ pr_lconstrarg c)
+
+        (* Auxiliary file and library management *)
+        | VernacAddLoadPath (fl,s,d) ->
+          return (
+            hov 2
+              (str"Add" ++
+                 (if fl then str" Rec " else spc()) ++
+                 str"LoadPath" ++ spc() ++ qs s ++
+                 (match d with
+                   | None -> mt()
+                   | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir))
+          )
+        | VernacRemoveLoadPath s ->
+          return (str"Remove LoadPath" ++ qs s)
+        | VernacAddMLPath (fl,s) ->
+          return (
+            str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s
+          )
+        | VernacDeclareMLModule (l) ->
+          return (
+            hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
+          )
+        | VernacChdir s ->
+          return (str"Cd" ++ pr_opt qs s)
+
+        (* Commands *)
+        | VernacDeclareTacticDefinition (rc,l) ->
+          let pr_tac_body (id, redef, body) =
+            let idl, body =
+              match body with
+                | Tacexpr.TacFun (idl,b) -> idl,b
+                | _ -> [], body in
+            pr_ltac_ref id ++
+              prlist (function None -> str " _"
+                | Some id -> spc () ++ pr_id id) idl
+            ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
+              pr_raw_tactic body
+          in
+          return (
+            hov 1
+              (str "Ltac " ++
+                 prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
+          )
+        | VernacCreateHintDb (dbname,b) ->
+          return (
+            hov 1 (str "Create HintDb " ++
+                     str dbname ++ (if b then str" discriminated" else mt ()))
+          )
+        | VernacRemoveHints (dbnames, ids) ->
+          return (
+            hov 1 (str "Remove Hints " ++
+                     prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
+                     pr_opt_hintbases dbnames)
+          )
+        | VernacHints (_, dbnames,h) ->
+          return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
+        | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) ->
+          return (
+            hov 2
+              (str"Notation " ++ pr_lident id ++ spc () ++
+                 prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
+                 pr_syntax_modifiers
+                 (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v]))
+          )
+        | VernacDeclareImplicits (q,[]) ->
+          return (
+            hov 2 (str"Implicit Arguments" ++ spc() ++ pr_smart_global q)
+          )
+        | VernacDeclareImplicits (q,impls) ->
+          return (
+            hov 1 (str"Implicit Arguments " ++
+                     spc() ++ pr_smart_global q ++ spc() ++
+                     prlist_with_sep spc (fun imps ->
+                       str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
+                     impls)
+          )
+        | VernacArguments (q, impl, nargs, mods) ->
+          return (
+            hov 2 (
+              str"Arguments" ++ spc() ++
+                pr_smart_global q ++
+                let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
+                let pr_if b x = if b then x else str "" in
+                let pr_br imp max x = match imp, max with
+                  | true, false -> str "[" ++ x ++ str "]"
+                  | true, true -> str "{" ++ x ++ str "}"
+                  | _ -> x in
+                let rec aux n l =
+                  match n, l with
+                    | 0, l -> spc () ++ str"/" ++ aux ~-1 l
+                    | _, [] -> mt()
+                    | n, (id,k,s,imp,max) :: tl ->
+                      spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
+                        aux (n-1) tl in
+                prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
+                  if not (List.is_empty mods) then str" : " else str"" ++
+                    prlist_with_sep (fun () -> str", " ++ spc()) (function
+                      | `ReductionDontExposeCase -> str "simpl nomatch"
+                      | `ReductionNeverUnfold -> str "simpl never"
+                      | `DefaultImplicits -> str "default implicits"
+                      | `Rename -> str "rename"
+                      | `Assert -> str "assert"
+                      | `ExtraScopes -> str "extra scopes"
+                      | `ClearImplicits -> str "clear implicits"
+                      | `ClearScopes -> str "clear scopes")
+                    mods)
+          )
+        | VernacReserve bl ->
+          let n = List.length (List.flatten (List.map fst bl)) in
+          return (
+            hov 2 (str"Implicit Type" ++
+                     str (if n > 1 then "s " else " ") ++
+                     pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
+          )
+        | VernacGeneralizable g ->
+          return (
+            hov 1 (str"Generalizable Variable" ++
+                     match g with
+                       | None -> str "s none"
+                       | Some [] -> str "s all"
+                       | Some idl ->
+                         str (if List.length idl > 1 then "s " else " ") ++
+                           prlist_with_sep spc pr_lident idl)
+          )
+        | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k ->
+          return (
+            hov 1 (str "Transparent" ++
+                     spc() ++ prlist_with_sep sep pr_smart_global l)
+          )
+        | VernacSetOpacity(Conv_oracle.Opaque,l) ->
+          return (
+            hov 1 (str "Opaque" ++
+                     spc() ++ prlist_with_sep sep pr_smart_global l)
+          )
+        | VernacSetOpacity _ ->
+          return (
+            Errors.anomaly (str "VernacSetOpacity used to set something else")
+          )
+        | VernacSetStrategy l ->
+          let pr_lev = function
+            | Conv_oracle.Opaque -> str"opaque"
+            | Conv_oracle.Expand -> str"expand"
+            | l when Conv_oracle.is_transparent l -> str"transparent"
+            | Conv_oracle.Level n -> int n
+          in
+          let pr_line (l,q) =
+            hov 2 (pr_lev l ++ spc() ++
+                     str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]")
+          in
+          return (
+            hov 1 (str "Strategy" ++ spc() ++
+                     hv 0 (prlist_with_sep sep pr_line l))
+          )
+        | VernacUnsetOption (na) ->
+          return (
+            hov 1 (str"Unset" ++ spc() ++ pr_printoption na None)
+          )
+        | VernacSetOption (na,v) ->
+          return (
+            hov 2 (str"Set" ++ spc() ++ pr_set_option na v)
+          )
+        | VernacAddOption (na,l) ->
+          return (
+            hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l))
+          )
+        | VernacRemoveOption (na,l) ->
+          return (
+            hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l))
+          )
+        | VernacMemOption (na,l) ->
+          return (
+            hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l))
+          )
+        | VernacPrintOption na ->
+          return (
+            hov 2 (str"Test" ++ spc() ++ pr_printoption na None)
+          )
+        | VernacCheckMayEval (r,io,c) ->
+          let pr_mayeval r c = match r with
+            | Some r0 ->
+              hov 2 (str"Eval" ++ spc() ++
+                       pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++
+                       spc() ++ str"in" ++ spc () ++ pr_lconstr c)
+            | None -> hov 2 (str"Check" ++ spc() ++ pr_lconstr c)
+          in
+          let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in
+          return (pr_i ++ pr_mayeval r c)
+        | VernacGlobalCheck c ->
+          return (hov 2 (str"Type" ++ pr_constrarg c))
+        | VernacDeclareReduction (s,r) ->
+          return (
+            str "Declare Reduction " ++ str s ++ str " := " ++
+              pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r
+          )
+        | VernacPrint p ->
+          return (pr_printable p)
+        | VernacSearch (sea,sea_r) ->
+          return (pr_search sea sea_r pr_constr_pattern_expr)
+        | VernacLocate loc ->
+          let pr_locate =function
+            | LocateAny qid -> pr_smart_global qid
+            | LocateTerm qid -> str "Term" ++ spc() ++ pr_smart_global qid
+            | LocateFile f -> str"File" ++ spc() ++ qs f
+            | LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid
+            | LocateModule qid -> str"Module" ++ spc () ++ pr_module qid
+            | LocateTactic qid -> str"Ltac" ++ spc () ++ pr_ltac_ref qid
+          in
+          return (str"Locate" ++ spc() ++ pr_locate loc)
+        | VernacRegister (id, RegisterInline) ->
+          return (
+            hov 2
+              (str "Register Inline" ++ spc() ++ pr_lident id)
+          )
+        | VernacComments l ->
+          return (
+            hov 2
+              (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l)
+          )
+        | VernacNop ->
+          mt()
+
+        (* Toplevel control *)
+        | VernacToplevelControl exn ->
+          return (pr_topcmd exn)
+
+        (* For extension *)
+        | VernacExtend (s,c) ->
+          return (pr_extend s c)
+        | VernacProof (None, None) ->
+          return (str "Proof")
+        | VernacProof (None, Some e) ->
+          return (str "Proof " ++ pr_using e)
+        | VernacProof (Some te, None) ->
+          return (str "Proof with" ++ spc() ++ pr_raw_tactic te)
+        | VernacProof (Some te, Some e) ->
+          return (
+            str "Proof " ++ pr_using e ++ spc() ++
+              str "with" ++ spc() ++pr_raw_tactic te
+          )
+        | VernacProofMode s ->
+          return (str ("Proof Mode "^s))
+        | VernacBullet b ->
+          return (begin match b with
+            | Dash n -> str (String.make n '-')
+            | Star n -> str (String.make n '*')
+            | Plus n -> str (String.make n '+')
+          end ++ spc())
+        | VernacSubproof None ->
+          return (str "{")
+        | VernacSubproof (Some i) ->
+          return (str "BeginSubproof " ++ int i)
+        | VernacEndSubproof ->
+          return (str "}")
+>>>>>>> Ppannotation.t: New constructor AVernac.
 
     and pr_vernac_list l =
       hov 2 (str"[" ++ spc() ++
@@ -1010,4 +1211,21 @@ module Make (Ppconstr : Ppconstrsig.Pp) = struct
 
 end
 
-include Make (Ppconstr)
+include Make (Ppconstr) (struct
+  let do_not_tag _ x = x
+  let tag_vernac = do_not_tag
+end)
+
+module RichPp (Indexer : sig
+  val index : Ppannotation.t -> string
+end) = struct
+
+  include Make (Ppconstr.RichPp (Indexer)) (struct
+    open Ppannotation
+
+    let tag_vernac v t =
+      Pp.open_tag (Indexer.index (AVernac v)) ++ t ++ Pp.close_tag ()
+
+  end)
+
+end