Imported Upstream version 8.5~beta1+dfsg

29 files changed, 6803 insertions, 0 deletions

diff --git a/printing/genprint.ml b/printing/genprint.ml
new file mode 100644
index 00000000..ade69ef8
--- /dev/null
+++ b/printing/genprint.ml
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Genarg
+
+type ('raw, 'glb, 'top) printer = {
+  raw : 'raw -> std_ppcmds;
+  glb : 'glb -> std_ppcmds;
+  top : 'top -> std_ppcmds;
+}
+
+module PrintObj =
+struct
+  type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) printer
+  let name = "printer"
+  let default wit = match unquote (rawwit wit) with
+  | ExtraArgType name ->
+    let printer = {
+      raw = (fun _ -> str "<genarg:" ++ str name ++ str ">");
+      glb = (fun _ -> str "<genarg:" ++ str name ++ str ">");
+      top = (fun _ -> str "<genarg:" ++ str name ++ str ">");
+    } in
+    Some printer
+  | _ -> assert false
+end
+
+module Print = Register (PrintObj)
+
+let register_print0 wit raw glb top =
+  let printer = { raw; glb; top; } in
+  Print.register0 wit printer
+
+let raw_print wit v = (Print.obj wit).raw v
+let glb_print wit v = (Print.obj wit).glb v
+let top_print wit v = (Print.obj wit).top v
+
+let generic_raw_print v = unpack { unpacker = fun w v -> raw_print w (raw v); } v
+let generic_glb_print v = unpack { unpacker = fun w v -> glb_print w (glb v); } v
+let generic_top_print v = unpack { unpacker = fun w v -> top_print w (top v); } v
diff --git a/printing/genprint.mli b/printing/genprint.mli
new file mode 100644
index 00000000..5b91d6d2
--- /dev/null
+++ b/printing/genprint.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Entry point for generic printers *)
+
+open Pp
+open Genarg
+
+val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> std_ppcmds
+(** Printer for raw level generic arguments. *)
+
+val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> std_ppcmds
+(** Printer for glob level generic arguments. *)
+
+val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> std_ppcmds
+(** Printer for top level generic arguments. *)
+
+val generic_raw_print : rlevel generic_argument -> std_ppcmds
+val generic_glb_print : glevel generic_argument -> std_ppcmds
+val generic_top_print : tlevel generic_argument -> std_ppcmds
+
+val register_print0 : ('raw, 'glb, 'top) genarg_type ->
+  ('raw -> std_ppcmds) -> ('glb -> std_ppcmds) -> ('top -> std_ppcmds) -> unit
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
new file mode 100644
index 00000000..d09af6d2
--- /dev/null
+++ b/printing/miscprint.ml
@@ -0,0 +1,49 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Misctypes
+open Pp
+
+(** Printing of [intro_pattern] *)
+
+let rec pr_intro_pattern prc (_,pat) = match pat with
+  | IntroForthcoming true -> str "*"
+  | IntroForthcoming false -> str "**"
+  | IntroNaming p -> pr_intro_pattern_naming p
+  | IntroAction p -> pr_intro_pattern_action prc p
+
+and pr_intro_pattern_naming = function
+  | IntroIdentifier id -> Nameops.pr_id id
+  | IntroFresh id -> str "?" ++ Nameops.pr_id id
+  | IntroAnonymous -> str "?"
+
+and pr_intro_pattern_action prc = function
+  | IntroWildcard -> str "_"
+  | IntroOrAndPattern pll -> pr_or_and_intro_pattern prc pll
+  | IntroInjection pl ->
+      str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++
+      str "]"
+  | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "/" ++ prc c
+  | IntroRewrite true -> str "->"
+  | IntroRewrite false -> str "<-"
+
+and pr_or_and_intro_pattern prc = function
+  | [pl] ->
+      str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")"
+  | pll ->
+      str "[" ++
+      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
+      ++ str "]"
+
+(** Printing of [move_location] *)
+
+let pr_move_location pr_id = function
+  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
+  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
+  | MoveFirst -> str " at top"
+  | MoveLast -> str " at bottom"
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
new file mode 100644
index 00000000..1d915ef8
--- /dev/null
+++ b/printing/miscprint.mli
@@ -0,0 +1,24 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Misctypes
+
+(** Printing of [intro_pattern] *)
+
+val pr_intro_pattern :
+  ('a -> Pp.std_ppcmds) -> 'a intro_pattern_expr Loc.located -> Pp.std_ppcmds
+
+val pr_or_and_intro_pattern :
+  ('a -> Pp.std_ppcmds) -> 'a or_and_intro_pattern_expr -> Pp.std_ppcmds
+
+val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds
+
+(** Printing of [move_location] *)
+
+val pr_move_location :
+  ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
new file mode 100644
index 00000000..4f26b824
--- /dev/null
+++ b/printing/ppannotation.ml
@@ -0,0 +1,41 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Ppextend
+open Constrexpr
+open Vernacexpr
+open Tacexpr
+
+type t =
+  | AKeyword
+  | 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"
+  | 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 =
+  []
+
+let tag = Pp.Tag.create "ppannotation"
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
new file mode 100644
index 00000000..bc345c34
--- /dev/null
+++ b/printing/ppannotation.mli
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This module defines the annotations that are attached to
+    semi-structured pretty-printing of Coq syntactic objects. *)
+
+open Ppextend
+open Constrexpr
+open Vernacexpr
+open Tacexpr
+
+type t =
+  | AKeyword
+  | 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
+
+val attributes_of_annotation : t -> (string * string) list
+
+val tag : t Pp.Tag.key
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
new file mode 100644
index 00000000..d9d8af66
--- /dev/null
+++ b/printing/ppconstr.ml
@@ -0,0 +1,812 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i*)
+open Errors
+open Util
+open Pp
+open Names
+open Nameops
+open Libnames
+open Pputils
+open Ppextend
+open Constrexpr
+open Constrexpr_ops
+open Decl_kinds
+open Misctypes
+(*i*)
+
+module Make (Taggers : sig
+  val tag_keyword     : std_ppcmds -> std_ppcmds
+  val tag_evar     : std_ppcmds -> std_ppcmds
+  val tag_type     : std_ppcmds -> std_ppcmds
+  val tag_path     : std_ppcmds -> std_ppcmds
+  val tag_ref     : std_ppcmds -> std_ppcmds
+  val tag_var     : std_ppcmds -> std_ppcmds
+  val tag_constr_expr : constr_expr -> std_ppcmds -> std_ppcmds
+  val tag_unparsing   : unparsing -> std_ppcmds -> std_ppcmds
+end) = struct
+
+  open Taggers
+
+  let keyword s = tag_keyword (str s)
+  let sep_v = fun _ -> str"," ++ spc()
+  let pr_tight_coma () = str "," ++ cut ()
+
+  let latom = 0
+  let lprod = 200
+  let llambda = 200
+  let lif = 200
+  let lletin = 200
+  let lletpattern = 200
+  let lfix = 200
+  let lcast = 100
+  let larg = 9
+  let lapp = 10
+  let lposint = 0
+  let lnegint = 35 (* must be consistent with Notation "- x" *)
+  let ltop = (200,E)
+  let lproj = 1
+  let ldelim = 1
+  let lsimpleconstr = (8,E)
+  let lsimplepatt = (1,E)
+
+  let prec_less child (parent,assoc) =
+    if parent < 0 && Int.equal child lprod then true
+    else
+      let parent = abs parent in
+      match assoc with
+        | E -> (<=) child parent
+        | L -> (<) child parent
+        | Prec n -> child<=n
+        | Any -> true
+
+  let prec_of_prim_token = function
+    | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
+    | String _ -> latom
+
+  open Notation
+
+  let print_hunks n pr pr_binders (terms, termlists, binders) unps =
+    let env = ref terms and envlist = ref termlists and bll = ref binders in
+    let pop r = let a = List.hd !r in r := List.tl !r; a in
+    let return unp pp1 pp2 = (tag_unparsing unp pp1) ++ pp2 in
+    (* Warning:
+       The following function enforces a very precise order of
+       evaluation of sub-components.
+       Do not modify it unless you know what you are doing! *)
+    let rec aux = function
+      | [] ->
+        mt ()
+      | UnpMetaVar (_, prec) as unp :: l ->
+        let c = pop env in
+        let pp2 = aux l in
+        let pp1 = pr (n, prec) c in
+        return unp pp1 pp2
+      | UnpListMetaVar (_, prec, sl) as unp :: l ->
+        let cl = pop envlist in
+        let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in
+        let pp2 = aux l in
+        return unp pp1 pp2
+      | UnpBinderListMetaVar (_, isopen, sl) as unp :: l ->
+        let cl = pop bll in
+        let pp2 = aux l in
+        let pp1 = pr_binders (fun () -> aux sl) isopen cl in
+        return unp pp1 pp2
+      | UnpTerminal s as unp :: l ->
+        let pp2 = aux l in
+        let pp1 = str s in
+        return unp pp1 pp2
+      | UnpBox (b,sub) as unp :: l ->
+        let pp1 = ppcmd_of_box b (aux sub) in
+        let pp2 = aux l in
+        return unp pp1 pp2
+      | UnpCut cut as unp :: l ->
+        let pp2 = aux l in
+        let pp1 = ppcmd_of_cut cut in
+        return unp pp1 pp2
+    in
+    aux unps
+
+  let pr_notation pr pr_binders s env =
+    let unpl, level = find_notation_printing_rule s in
+    print_hunks level pr pr_binders env unpl, level
+
+  let pr_delimiters key strm =
+    strm ++ str ("%"^key)
+
+  let pr_generalization bk ak c =
+    let hd, tl =
+      match bk with
+        | Implicit -> "{", "}"
+        | Explicit -> "(", ")"
+    in (* TODO: syntax Abstraction Kind *)
+    str "`" ++ str hd ++ c ++ str tl
+
+  let pr_com_at n =
+    if Flags.do_beautify() && not (Int.equal n 0) then comment n
+    else mt()
+
+  let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
+
+  let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
+
+  let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
+
+  let pr_univ l =
+    match l with
+      | [x] -> str x
+      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")"
+
+  let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
+
+  let pr_glob_sort = function
+    | GProp -> tag_type (str "Prop")
+    | GSet -> tag_type (str "Set")
+    | GType [] -> tag_type (str "Type")
+    | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
+
+  let pr_qualid sp =
+    let (sl, id) = repr_qualid sp in
+    let id = tag_ref (str (Id.to_string id)) in
+    let sl = match List.rev (DirPath.repr sl) with
+    | [] -> mt ()
+    | sl ->
+      let pr dir = tag_path (str (Id.to_string dir)) ++ str "." in
+      prlist pr sl
+    in
+    sl ++ id
+
+  let pr_id = pr_id
+  let pr_name = pr_name
+  let pr_qualid = pr_qualid
+  let pr_patvar = pr_id
+
+  let pr_glob_sort_instance = function
+    | GProp ->
+      tag_type (str "Prop")
+    | GSet ->
+      tag_type (str "Set")
+    | GType u ->
+      (match u with
+        | Some u -> str u
+        | None -> tag_type (str "Type"))
+
+  let pr_universe_instance l =
+    pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l
+
+  let pr_reference = function
+  | Qualid (_, qid) -> pr_qualid qid
+  | Ident (_, id) -> tag_var (str (Id.to_string id))
+
+  let pr_cref ref us =
+    pr_reference ref ++ pr_universe_instance us
+
+  let pr_expl_args pr (a,expl) =
+    match expl with
+      | None -> pr (lapp,L) a
+      | Some (_,ExplByPos (n,_id)) ->
+        anomaly (Pp.str "Explicitation by position not implemented")
+      | Some (_,ExplByName id) ->
+        str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
+
+  let pr_opt_type pr = function
+    | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt ()
+    | t -> cut () ++ str ":" ++ pr t
+
+  let pr_opt_type_spc pr = function
+    | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt ()
+    | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
+
+  let pr_lident (loc,id) =
+    if not (Loc.is_ghost loc) then
+      let (b,_) = Loc.unloc loc in
+      pr_located pr_id (Loc.make_loc (b,b + String.length (Id.to_string id)), id)
+    else
+      pr_id id
+
+  let pr_lname = function
+    | (loc,Name id) -> pr_lident (loc,id)
+    | lna -> pr_located pr_name lna
+
+  let pr_or_var pr = function
+    | ArgArg x -> pr x
+    | ArgVar (loc,s) -> pr_lident (loc,s)
+
+  let pr_prim_token = function
+    | Numeral n -> str (Bigint.to_string n)
+    | String s -> qs s
+
+  let pr_evar pr id l =
+    hov 0 (
+      tag_evar (str "?" ++ pr_id id) ++
+        (match l with
+          | [] -> mt()
+          | l ->
+            let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in
+            str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}"))
+
+  let las = lapp
+  let lpator = 100
+  let lpatrec = 0
+
+  let rec pr_patt sep inh p =
+    let (strm,prec) = match p with
+      | CPatRecord (_, l) ->
+        let pp (c, p) =
+          pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p
+        in
+        str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec
+
+      | CPatAlias (_, p, id) ->
+        pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
+
+      | CPatCstr (_,c, [], []) ->
+        pr_reference c, latom
+
+      | CPatCstr (_, c, [], args) ->
+        pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
+
+      | CPatCstr (_, c, args, []) ->
+        str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
+
+      | CPatCstr (_, c, expl_args, extra_args) ->
+        surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args)
+        ++ prlist (pr_patt spc (lapp,L)) extra_args, lapp
+
+      | CPatAtom (_, None) ->
+        str "_", latom
+
+      | CPatAtom (_,Some r) ->
+        pr_reference r, latom
+
+      | CPatOr (_,pl) ->
+        hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator
+
+      | CPatNotation (_,"( _ )",([p],[]),[]) ->
+        pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
+
+      | CPatNotation (_,s,(l,ll),args) ->
+        let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) in
+        (if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not)
+        ++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not
+
+      | CPatPrim (_,p) ->
+        pr_prim_token p, latom
+
+      | CPatDelimiters (_,k,p) ->
+        pr_delimiters k (pr_patt mt lsimplepatt p), 1
+    in
+    let loc = cases_pattern_expr_loc p in
+    pr_with_comments loc
+      (sep() ++ if prec_less prec inh then strm else surround strm)
+
+  let pr_patt = pr_patt mt
+
+  let pr_eqn pr (loc,pl,rhs) =
+    let pl = List.map snd pl in
+    spc() ++ hov 4
+      (pr_with_comments loc
+         (str "| " ++
+            hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl
+                   ++ str " =>") ++
+            pr_sep_com spc (pr ltop) rhs))
+
+  let begin_of_binder = function
+  LocalRawDef((loc,_),_) -> fst (Loc.unloc loc)
+    | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
+    | _ -> assert false
+
+  let begin_of_binders = function
+    | b::_ -> begin_of_binder b
+    | _ -> 0
+
+  let surround_impl k p =
+    match k with
+      | Explicit -> str"(" ++ p ++ str")"
+      | Implicit -> str"{" ++ p ++ str"}"
+
+  let surround_implicit k p =
+    match k with
+      | Explicit -> p
+      | Implicit -> (str"{" ++ p ++ str"}")
+
+  let pr_binder many pr (nal,k,t) =
+    match k with
+      | Generalized (b, b', t') ->
+        assert (match b with Implicit -> true | _ -> false);
+        begin match nal with
+          |[loc,Anonymous] ->
+            hov 1 (str"`" ++ (surround_impl b'
+                                ((if t' then str "!" else mt ()) ++ pr t)))
+          |[loc,Name id] ->
+            hov 1 (str "`" ++ (surround_impl b'
+                                 (pr_lident (loc,id) ++ str " : " ++
+                                    (if t' then str "!" else mt()) ++ pr t)))
+          |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.")
+        end
+      | Default b ->
+        match t with
+          | CHole (_,_,Misctypes.IntroAnonymous,_) ->
+            let s = prlist_with_sep spc pr_lname nal in
+            hov 1 (surround_implicit b s)
+          | _ ->
+            let s = prlist_with_sep spc pr_lname nal ++ str " : " ++ pr t in
+            hov 1 (if many then surround_impl b s else surround_implicit b s)
+
+  let pr_binder_among_many pr_c = function
+    | LocalRawAssum (nal,k,t) ->
+      pr_binder true pr_c (nal,k,t)
+    | LocalRawDef (na,c) ->
+      let c,topt = match c with
+        | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t
+        | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
+      surround (pr_lname na ++ pr_opt_type pr_c topt ++
+                  str":=" ++ cut() ++ pr_c c)
+
+  let pr_undelimited_binders sep pr_c =
+    prlist_with_sep sep (pr_binder_among_many pr_c)
+
+  let pr_delimited_binders kw sep pr_c bl =
+    let n = begin_of_binders bl in
+    match bl with
+      | [LocalRawAssum (nal,k,t)] ->
+        pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t)
+      | LocalRawAssum _ :: _ as bdl ->
+        pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl
+      | _ -> assert false
+
+  let pr_binders_gen pr_c sep is_open =
+    if is_open then pr_delimited_binders mt sep pr_c
+    else pr_undelimited_binders sep pr_c
+
+  let rec extract_prod_binders = function
+  (*  | CLetIn (loc,na,b,c) as x ->
+      let bl,c = extract_prod_binders c in
+      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
+    | CProdN (loc,[],c) ->
+      extract_prod_binders c
+    | CProdN (loc,(nal,bk,t)::bl,c) ->
+      let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
+      LocalRawAssum (nal,bk,t) :: bl, c
+    | c -> [], c
+
+  let rec extract_lam_binders = function
+  (*  | CLetIn (loc,na,b,c) as x ->
+      let bl,c = extract_lam_binders c in
+      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
+    | CLambdaN (loc,[],c) ->
+      extract_lam_binders c
+    | CLambdaN (loc,(nal,bk,t)::bl,c) ->
+      let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
+      LocalRawAssum (nal,bk,t) :: bl, c
+    | c -> [], c
+
+  let split_lambda = function
+    | CLambdaN (loc,[[na],bk,t],c) -> (na,t,c)
+    | CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
+    | CLambdaN (loc,(na::nal,bk,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,bk,t)::bl,c))
+    | _ -> anomaly (Pp.str "ill-formed fixpoint body")
+
+  let rename na na' t c =
+    match (na,na') with
+      | (_,Name id), (_,Name id') ->
+        (na',t,Topconstr.replace_vars_constr_expr (Id.Map.singleton id id') c)
+      | (_,Name id), (_,Anonymous) -> (na,t,c)
+      | _ -> (na',t,c)
+
+  let split_product na' = function
+    | CProdN (loc,[[na],bk,t],c) -> rename na na' t c
+    | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
+    | CProdN (loc,(na::nal,bk,t)::bl,c) ->
+      rename na na' t (CProdN(loc,(nal,bk,t)::bl,c))
+    | _ -> anomaly (Pp.str "ill-formed fixpoint body")
+
+  let rec split_fix n typ def =
+    if Int.equal n 0 then ([],typ,def)
+    else
+      let (na,_,def) = split_lambda def in
+      let (na,t,typ) = split_product na typ in
+      let (bl,typ,def) = split_fix (n-1) typ def in
+      (LocalRawAssum ([na],default_binder_kind,t)::bl,typ,def)
+
+  let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
+    let pr_body =
+      if dangling_with_for then pr_dangling else pr in
+    pr_id id ++ str" " ++
+      hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++
+      pr_opt_type_spc pr t ++ str " :=" ++
+      pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
+
+  let pr_guard_annot pr_aux bl (n,ro) =
+    match n with
+      | None -> mt ()
+      | Some (loc, id) ->
+        match (ro : Constrexpr.recursion_order_expr) with
+          | CStructRec ->
+            let names_of_binder = function
+              | LocalRawAssum (nal,_,_) -> nal
+              | LocalRawDef (_,_) -> []
+            in let ids = List.flatten (List.map names_of_binder bl) in
+               if List.length ids > 1 then
+                 spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}"
+               else mt()
+          | CWfRec c ->
+            spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_id id ++ str"}"
+          | CMeasureRec (m,r) ->
+            spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++
+              (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}"
+
+  let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) =
+    let annot = pr_guard_annot (pr lsimpleconstr) bl ro in
+    pr_recursive_decl pr prd dangling_with_for id bl annot t c
+
+  let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) =
+    pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
+
+  let pr_recursive pr_decl id = function
+    | [] -> anomaly (Pp.str "(co)fixpoint with no definition")
+    | [d1] -> pr_decl false d1
+    | dl ->
+      prlist_with_sep (fun () -> fnl() ++ keyword "with" ++ spc ())
+        (pr_decl true) dl ++
+        fnl() ++ keyword "for" ++ spc () ++ pr_id id
+
+  let pr_asin pr (na,indnalopt) =
+    (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
+      | Some na -> spc () ++ keyword "as" ++ spc () ++  pr_lname na
+      | None -> mt ()) ++
+      (match indnalopt with
+        | None -> mt ()
+        | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t)
+
+  let pr_case_item pr (tm,asin) =
+    hov 0 (pr (lcast,E) tm ++ pr_asin pr asin)
+
+  let pr_case_type pr po =
+    match po with
+      | None | Some (CHole (_,_,Misctypes.IntroAnonymous,_)) -> mt()
+      | Some p ->
+        spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p)
+
+  let pr_simple_return_type pr na po =
+    (match na with
+      | Some (_,Name id) ->
+        spc () ++ keyword "as" ++ spc () ++ pr_id id
+      | _ -> mt ()) ++
+      pr_case_type pr po
+
+  let pr_proj pr pr_app a f l =
+    hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
+
+  let pr_appexpl pr (f,us) l =
+    hov 2 (
+      str "@" ++ pr_reference f ++
+        pr_universe_instance us ++
+        prlist (pr_sep_com spc (pr (lapp,L))) l)
+
+  let pr_app pr a l =
+    hov 2 (
+      pr (lapp,L) a  ++
+        prlist (fun a -> spc () ++ pr_expl_args pr a) l)
+
+  let pr_forall () = keyword "forall" ++ spc ()
+
+  let pr_fun () = keyword "fun" ++ spc ()
+
+  let pr_fun_sep = spc () ++ str "=>"
+
+  let pr_dangling_with_for sep pr inherited a =
+    match a with
+      | (CFix (_,_,[_])|CCoFix(_,_,[_])) ->
+        pr sep (latom,E) a
+      | _ ->
+        pr sep inherited a
+
+  let pr pr sep inherited a =
+    let return (cmds, prec) = (tag_constr_expr a cmds, prec) in
+    let (strm, prec) = match a with
+      | CRef (r, us) ->
+        return (pr_cref r us, latom)
+      | CFix (_,id,fix) ->
+        return (
+          hov 0 (keyword "fix" ++ spc () ++
+                   pr_recursive
+                   (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix),
+          lfix
+        )
+      | CCoFix (_,id,cofix) ->
+        return (
+          hov 0 (keyword "cofix" ++ spc () ++
+                   pr_recursive
+                   (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix),
+          lfix
+        )
+      | CProdN _ ->
+        let (bl,a) = extract_prod_binders a in
+        return (
+          hov 0 (
+            hov 2 (pr_delimited_binders pr_forall spc
+                     (pr mt ltop) bl) ++
+              str "," ++ pr spc ltop a),
+          lprod
+        )
+      | CLambdaN _ ->
+        let (bl,a) = extract_lam_binders a in
+        return (
+          hov 0 (
+            hov 2 (pr_delimited_binders pr_fun spc
+                     (pr mt ltop) bl) ++
+              pr_fun_sep ++ pr spc ltop a),
+          llambda
+        )
+      | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
+          when Id.equal x x' ->
+        return (
+          hv 0 (
+            hov 2 (keyword "let" ++ spc () ++ pr mt ltop fx
+                   ++ spc ()
+                   ++ keyword "in") ++
+              pr spc ltop b),
+          lletin
+        )
+      | CLetIn (_,x,a,b) ->
+        return (
+          hv 0 (
+            hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :="
+                   ++ pr spc ltop a ++ spc ()
+                   ++ keyword "in") ++
+              pr spc ltop b),
+          lletin
+        )
+      | CAppExpl (_,(Some i,f,us),l) ->
+        let l1,l2 = List.chop i l in
+        let c,l1 = List.sep_last l1 in
+        let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in
+        if not (List.is_empty l2) then
+          return (p ++ prlist (pr spc (lapp,L)) l2, lapp)
+        else
+          return (p, lproj)
+      | CAppExpl (_,(None,Ident (_,var),us),[t])
+      | CApp (_,(_,CRef(Ident(_,var),us)),[t,None])
+          when Id.equal var Notation_ops.ldots_var ->
+        return (
+          hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."),
+          larg
+        )
+      | CAppExpl (_,(None,f,us),l) ->
+        return (pr_appexpl (pr mt) (f,us) l, lapp)
+      | CApp (_,(Some i,f),l) ->
+        let l1,l2 = List.chop i l in
+        let c,l1 = List.sep_last l1 in
+        assert (Option.is_empty (snd c));
+        let p = pr_proj (pr mt) pr_app (fst c) f l1 in
+        if not (List.is_empty l2) then
+          return (
+            p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2,
+            lapp
+          )
+        else
+          return (p, lproj)
+      | CApp (_,(None,a),l) ->
+        return (pr_app (pr mt) a l, lapp)
+      | CRecord (_,w,l) ->
+        let beg =
+          match w with
+            | None ->
+              spc ()
+            | Some t ->
+              spc () ++ pr spc ltop t ++ spc ()
+              ++ keyword "with" ++ spc ()
+        in
+        return (
+          hv 0 (str"{|" ++ beg ++
+                  prlist_with_sep pr_semicolon
+                  (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l
+                ++ str" |}"),
+          latom
+        )
+      | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
+        return (
+          hv 0 (
+            keyword "let" ++ spc () ++ str"'" ++
+              hov 0 (pr_patt ltop p ++
+                       pr_asin (pr_dangling_with_for mt pr) asin ++
+                       str " :=" ++ pr spc ltop c ++
+                       pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++
+                       spc () ++ keyword "in" ++ pr spc ltop b)),
+          lletpattern
+        )
+      | CCases(_,_,rtntypopt,c,eqns) ->
+        return (
+          v 0
+            (hv 0 (keyword "match" ++ brk (1,2) ++
+                     hov 0 (
+                       prlist_with_sep sep_v
+                         (pr_case_item (pr_dangling_with_for mt pr)) c
+                       ++ pr_case_type (pr_dangling_with_for mt pr) rtntypopt) ++
+                     spc () ++ keyword "with") ++
+               prlist (pr_eqn (pr mt)) eqns ++ spc()
+             ++ keyword "end"),
+          latom
+        )
+      | CLetTuple (_,nal,(na,po),c,b) ->
+        return (
+          hv 0 (
+            keyword "let" ++ spc () ++
+              hov 0 (str "(" ++
+                       prlist_with_sep sep_v pr_lname nal ++
+                       str ")" ++
+                       pr_simple_return_type (pr mt) na po ++ str " :=" ++
+                       pr spc ltop c ++ spc ()
+                     ++ keyword "in") ++
+              pr spc ltop b),
+          lletin
+        )
+      | CIf (_,c,(na,po),b1,b2) ->
+      (* On force les parenthèses autour d'un "if" sous-terme (même si le
+         parsing est lui plus tolérant) *)
+        return (
+          hv 0 (
+            hov 1 (keyword "if" ++ spc () ++ pr mt ltop c
+                   ++ pr_simple_return_type (pr mt) na po) ++
+              spc () ++
+              hov 0 (keyword "then"
+                     ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++
+              hov 0 (keyword "else" ++ pr (fun () -> brk (1,1)) ltop b2)),
+        lif
+        )
+
+      | CHole (_,_,Misctypes.IntroIdentifier id,_) ->
+        return (str "?[" ++ pr_id id ++ str "]", latom)
+      | CHole (_,_,Misctypes.IntroFresh id,_) ->
+        return (str "?[?" ++ pr_id id ++ str "]", latom)
+      | CHole (_,_,_,_) ->
+        return (str "_", latom)
+      | CEvar (_,n,l) ->
+        return (pr_evar (pr mt) n l, latom)
+      | CPatVar (_,p) ->
+        return (str "?" ++ pr_patvar p, latom)
+      | CSort (_,s) ->
+        return (pr_glob_sort s, latom)
+      | CCast (_,a,b) ->
+        return (
+          hv 0 (pr mt (lcast,L) a ++ cut () ++
+                  match b with
+                    | CastConv b -> str ":" ++ pr mt (-lcast,E) b
+                    | CastVM b -> str "<:" ++ pr mt (-lcast,E) b
+                    | CastNative b -> str "<<:" ++ pr mt (-lcast,E) b
+                    | CastCoerce -> str ":>"),
+          lcast
+        )
+      | CNotation (_,"( _ )",([t],[],[])) ->
+        return (pr (fun()->str"(") (max_int,L) t ++ str")", latom)
+      | CNotation (_,s,env) ->
+        pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env
+      | CGeneralization (_,bk,ak,c) ->
+        return (pr_generalization bk ak (pr mt ltop c), latom)
+      | CPrim (_,p) ->
+        return (pr_prim_token p, prec_of_prim_token p)
+      | CDelimiters (_,sc,a) ->
+        return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim)
+    in
+    let loc = constr_loc a in
+    pr_with_comments loc
+      (sep() ++ if prec_less prec inherited then strm else surround strm)
+
+  type term_pr = {
+    pr_constr_expr   : constr_expr -> std_ppcmds;
+    pr_lconstr_expr  : constr_expr -> std_ppcmds;
+    pr_constr_pattern_expr  : constr_pattern_expr -> std_ppcmds;
+    pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+  }
+
+  type precedence =  Ppextend.precedence * Ppextend.parenRelation
+  let modular_constr_pr = pr
+  let rec fix rf x = rf (fix rf) x
+  let pr = fix modular_constr_pr mt
+
+  let transf env c =
+    if !Flags.beautify_file then
+      let r = Constrintern.for_grammar (Constrintern.intern_constr env) c in
+      Constrextern.extern_glob_constr (Termops.vars_of_env env) r
+    else c
+
+  let pr prec c = pr prec (transf (Global.env()) c)
+
+  let pr_simpleconstr = function
+    | CAppExpl (_,(None,f,us),[]) -> str "@" ++ pr_cref f us
+    | c -> pr lsimpleconstr c
+
+  let default_term_pr = {
+    pr_constr_expr   = pr_simpleconstr;
+    pr_lconstr_expr  = pr ltop;
+    pr_constr_pattern_expr  = pr_simpleconstr;
+    pr_lconstr_pattern_expr = pr ltop
+  }
+
+  let term_pr = ref default_term_pr
+
+  let set_term_pr = (:=) term_pr
+
+  let pr_constr_expr c   = !term_pr.pr_constr_expr   c
+  let pr_lconstr_expr c  = !term_pr.pr_lconstr_expr  c
+  let pr_constr_pattern_expr c  = !term_pr.pr_constr_pattern_expr  c
+  let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c
+
+  let pr_cases_pattern_expr = pr_patt ltop
+
+  let pr_binders = pr_undelimited_binders spc (pr ltop)
+
+end
+
+module Tag =
+struct
+  let keyword =
+    let style = Terminal.make ~bold:true () in
+    Ppstyle.make ~style ["constr"; "keyword"]
+
+  let evar =
+    let style = Terminal.make ~fg_color:`LIGHT_BLUE () in
+    Ppstyle.make ~style ["constr"; "evar"]
+
+  let univ =
+    let style = Terminal.make ~bold:true ~fg_color:`YELLOW () in
+    Ppstyle.make ~style ["constr"; "type"]
+
+  let notation =
+    let style = Terminal.make ~fg_color:`WHITE () in
+    Ppstyle.make ~style ["constr"; "notation"]
+
+  let variable =
+    Ppstyle.make ["constr"; "variable"]
+
+  let reference =
+    let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
+    Ppstyle.make ~style ["constr"; "reference"]
+
+  let path =
+    let style = Terminal.make ~fg_color:`LIGHT_MAGENTA () in
+    Ppstyle.make ~style ["constr"; "path"]
+
+end
+
+let do_not_tag _ x = x
+
+(** Instantiating Make with tagging functions that only add style
+    information. *)
+include Make (struct
+    let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
+    let tag_keyword     = tag Tag.keyword
+    let tag_evar        = tag Tag.evar
+    let tag_type        = tag Tag.univ
+    let tag_unparsing   = function
+    | UnpTerminal s -> tag Tag.notation
+    | _ -> do_not_tag ()
+    let tag_constr_expr = do_not_tag
+    let tag_path = tag Tag.path
+    let tag_ref = tag Tag.reference
+    let tag_var = tag Tag.variable
+end)
+
+module Richpp = struct
+
+  include Make (struct
+    open Ppannotation
+    let tag_keyword       = Pp.tag (Pp.Tag.inj AKeyword tag)
+    let tag_type          = Pp.tag (Pp.Tag.inj AKeyword tag)
+    let tag_evar          = do_not_tag ()
+    let tag_unparsing unp = Pp.tag (Pp.Tag.inj (AUnparsing unp) tag)
+    let tag_constr_expr e = Pp.tag (Pp.Tag.inj (AConstrExpr e) tag)
+    let tag_path = do_not_tag ()
+    let tag_ref = do_not_tag ()
+    let tag_var = do_not_tag ()
+  end)
+
+end
+
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
new file mode 100644
index 00000000..6e8d3b04
--- /dev/null
+++ b/printing/ppconstr.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This module implements pretty-printers for constr_expr syntactic
+    objects and their subcomponents. *)
+
+(** The default pretty-printers produce {!Pp.std_ppcmds} that are
+    interpreted as raw strings. *)
+include Ppconstrsig.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}. *)
+
+module Richpp : Ppconstrsig.Pp
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
new file mode 100644
index 00000000..15413d51
--- /dev/null
+++ b/printing/ppconstrsig.mli
@@ -0,0 +1,95 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Loc
+open Pp
+open Libnames
+open Constrexpr
+open Names
+open Misctypes
+open Locus
+open Genredexpr
+
+module type Pp = sig
+
+  val extract_lam_binders :
+    constr_expr -> local_binder list * constr_expr
+  val extract_prod_binders :
+    constr_expr -> local_binder list * constr_expr
+  val split_fix :
+    int -> constr_expr -> constr_expr ->
+    local_binder list *  constr_expr * constr_expr
+
+  val prec_less : int -> int * Ppextend.parenRelation -> bool
+
+  val pr_tight_coma : unit -> std_ppcmds
+
+  val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+
+  val pr_lident : Id.t located -> std_ppcmds
+  val pr_lname : Name.t located -> std_ppcmds
+
+  val pr_with_comments : Loc.t -> std_ppcmds -> std_ppcmds
+  val pr_com_at : int -> std_ppcmds
+  val pr_sep_com :
+    (unit -> std_ppcmds) ->
+    (constr_expr -> std_ppcmds) ->
+    constr_expr -> std_ppcmds
+
+  val pr_id : Id.t -> std_ppcmds
+  val pr_name : Name.t -> std_ppcmds
+  val pr_qualid : qualid -> std_ppcmds
+  val pr_patvar : patvar -> std_ppcmds
+
+  val pr_glob_sort : glob_sort -> std_ppcmds
+  val pr_guard_annot : (constr_expr -> std_ppcmds) ->
+    local_binder list ->
+    ('a * Names.Id.t) option * recursion_order_expr ->
+    std_ppcmds
+
+  val pr_binders : local_binder list -> std_ppcmds
+  val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
+  val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+  val pr_constr_expr : constr_expr -> std_ppcmds
+  val pr_lconstr_expr : constr_expr -> std_ppcmds
+  val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
+
+  type term_pr = {
+    pr_constr_expr   : constr_expr -> std_ppcmds;
+    pr_lconstr_expr  : constr_expr -> std_ppcmds;
+    pr_constr_pattern_expr  : constr_pattern_expr -> std_ppcmds;
+    pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+  }
+
+  val set_term_pr : term_pr -> unit
+  val default_term_pr : term_pr
+
+(** The modular constr printer.
+    [modular_constr_pr pr s p t] prints the head of the term [t] and calls
+    [pr] on its subterms.
+    [s] is typically {!Pp.mt} and [p] is [lsimpleconstr] for "constr" printers
+    and [ltop] for "lconstr" printers (spiwack: we might need more
+    specification here).
+    We can make a new modular constr printer by overriding certain branches,
+    for instance if we want to build a printer which prints "Prop" as "Omega"
+    instead we can proceed as follows:
+    let my_modular_constr_pr pr s p = function
+    | CSort (_,GProp Null) -> str "Omega"
+    | t -> modular_constr_pr pr s p t
+    Which has the same type. We can turn a modular printer into a printer by
+    taking its fixpoint. *)
+
+  type precedence
+  val lsimpleconstr : precedence
+  val ltop : precedence
+  val modular_constr_pr :
+    ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) ->
+    (unit->std_ppcmds) -> precedence  -> constr_expr -> std_ppcmds
+
+end
+
diff --git a/printing/ppstyle.ml b/printing/ppstyle.ml
new file mode 100644
index 00000000..fb334c70
--- /dev/null
+++ b/printing/ppstyle.ml
@@ -0,0 +1,149 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+
+type t = string
+(** We use the concatenated string, with dots separating each string. We
+    forbid the use of dots in the strings. *)
+
+let tags : Terminal.style option String.Map.t ref = ref String.Map.empty
+
+let make ?style tag =
+  let check s = if String.contains s '.' then invalid_arg "Ppstyle.make" in
+  let () = List.iter check tag in
+  let name = String.concat "." tag in
+  let () = assert (not (String.Map.mem name !tags)) in
+  let () = tags := String.Map.add name style !tags in
+  name
+
+let repr t = String.split '.' t
+
+let get_style tag =
+  try String.Map.find tag !tags with Not_found -> assert false
+
+let set_style tag st =
+  try tags := String.Map.update tag st !tags with Not_found -> assert false
+
+let clear_styles () =
+  tags := String.Map.map (fun _ -> None) !tags
+
+let dump () = String.Map.bindings !tags
+
+let parse_config s =
+  let styles = Terminal.parse s in
+  let set accu (name, st) =
+    try String.Map.update name (Some st) accu with Not_found -> accu
+  in
+  tags := List.fold_left set !tags styles
+
+let tag = Pp.Tag.create "ppstyle"
+
+(** Default tag is to reset everything *)
+let default = Terminal.({
+  fg_color = Some `DEFAULT;
+  bg_color = Some `DEFAULT;
+  bold = Some false;
+  italic = Some false;
+  underline = Some false;
+  negative = Some false;
+})
+
+let empty = Terminal.make ()
+
+let make_style_stack style_tags =
+  (** Not thread-safe. We should put a lock somewhere if we print from
+      different threads. Do we? *)
+  let style_stack = ref [] in
+  let peek () = match !style_stack with
+  | [] -> default (** Anomalous case, but for robustness *)
+  | st :: _ -> st
+  in
+  let push tag =
+    let style =
+      try
+        begin match String.Map.find tag style_tags with
+        | None -> empty
+        | Some st -> st
+        end
+      with Not_found -> empty
+    in
+    (** Use the merging of the latest tag and the one being currently pushed.
+    This may be useful if for instance the latest tag changes the background and
+    the current one the foreground, so that the two effects are additioned. *)
+    let style = Terminal.merge (peek ()) style in
+    let () = style_stack := style :: !style_stack in
+    Terminal.eval style
+  in
+  let pop _ = match !style_stack with
+  | [] ->
+    (** Something went wrong, we fallback *)
+    Terminal.eval default
+  | _ :: rem ->
+    let () = style_stack := rem in
+    Terminal.eval (peek ())
+  in
+  let clear () = style_stack := [] in
+  push, pop, clear
+
+let error_tag =
+  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in
+  make ~style ["message"; "error"]
+
+let warning_tag =
+  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW () in
+  make ~style ["message"; "warning"]
+
+let debug_tag =
+  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA () in
+  make ~style ["message"; "debug"]
+
+let pp_tag t = match Pp.Tag.prj t tag with
+| None -> ""
+| Some key -> key
+
+let init_color_output () =
+  let push_tag, pop_tag, clear_tag = make_style_stack !tags in
+  let tag_handler = {
+    Format.mark_open_tag = push_tag;
+    Format.mark_close_tag = pop_tag;
+    Format.print_open_tag = ignore;
+    Format.print_close_tag = ignore;
+  } in
+  let open Pp_control in
+  let () = Format.pp_set_mark_tags !std_ft true in
+  let () = Format.pp_set_mark_tags !err_ft true in
+  let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in
+  let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in
+  let pptag = tag in
+  let open Pp in
+  let msg ?header ft strm =
+    let strm = match header with
+    | None -> hov 0 strm
+    | Some (h, t) ->
+      let tag = Pp.Tag.inj t pptag in
+      let h = Pp.tag tag (str h ++ str ":") in
+      hov 0 (h ++ spc () ++ strm)
+    in
+    pp_with ~pp_tag ft strm;
+    Format.pp_print_newline ft ();
+    Format.pp_print_flush ft ();
+    (** In case something went wrong, we reset the stack *)
+    clear_tag ();
+  in
+  let logger level strm = match level with
+  | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm
+  | Info -> msg !std_ft strm
+  | Notice -> msg !std_ft strm
+  | Warning ->
+    let header = ("Warning", warning_tag) in
+    Flags.if_warn (fun () -> msg ~header !err_ft strm) ()
+  | Error -> msg ~header:("Error", error_tag) !err_ft strm
+  in
+  let () = set_logger logger in
+  ()
diff --git a/printing/ppstyle.mli b/printing/ppstyle.mli
new file mode 100644
index 00000000..f5d6184c
--- /dev/null
+++ b/printing/ppstyle.mli
@@ -0,0 +1,70 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Highlighting of printers. Used for pretty-printing terms that should be
+    displayed on a color-capable terminal. *)
+
+(** {5 Style tags} *)
+
+type t
+(** Style tags *)
+
+val make : ?style:Terminal.style -> string list -> t
+(** Create a new tag with the given name. Each name must be unique. The optional
+    style is taken as the default one. *)
+
+val repr : t -> string list
+(** Gives back the original name of the style tag where each string has been
+    concatenated and separated with a dot. *)
+
+val tag : t Pp.Tag.key
+(** An annotation for styles *)
+
+(** {5 Manipulating global styles} *)
+
+val get_style : t -> Terminal.style option
+(** Get the style associated to a tag. *)
+
+val set_style : t -> Terminal.style option -> unit
+(** Set a style associated to a tag. *)
+
+val clear_styles : unit -> unit
+(** Clear all styles. *)
+
+val parse_config : string -> unit
+(** Add all styles from the given string as parsed by {!Terminal.parse}.
+    Unregistered tags are ignored. *)
+
+val dump : unit -> (t * Terminal.style option) list
+(** Recover the list of known tags together with their current style. *)
+
+(** {5 Setting color output} *)
+
+val init_color_output : unit -> unit
+(** Once called, all tags defined here will use their current style when
+    printed. To this end, this function redefines the loggers used when sending
+    messages to the user. The program will in particular use the formatters
+    {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages,
+    with additional syle information provided by this module. Be careful this is
+    not compatible with the Emacs mode! *)
+
+val pp_tag : Pp.tag_handler
+(** Returns the name of a style tag that is understandable by the formatters
+    that have been inititialized through {!init_color_output}. To be used with
+    {!Pp.pp_with}. *)
+
+(** {5 Tags} *)
+
+val error_tag : t
+(** Tag used by the {!Pp.msg_error} function. *)
+
+val warning_tag : t
+(** Tag used by the {!Pp.msg_warning} function. *)
+
+val debug_tag : t
+(** Tag used by the {!Pp.msg_debug} function. *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
new file mode 100644
index 00000000..f8264e5a
--- /dev/null
+++ b/printing/pptactic.ml
@@ -0,0 +1,1499 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+open Namegen
+open Errors
+open Util
+open Constrexpr
+open Tacexpr
+open Genarg
+open Constrarg
+open Libnames
+open Ppextend
+open Misctypes
+open Locus
+open Decl_kinds
+open Genredexpr
+open Ppconstr
+open Printer
+
+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_primitive
+        : std_ppcmds -> std_ppcmds
+      val tag_string
+        : 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 primitive x = tag_primitive (str x)
+
+  let pr_with_occurrences pr (occs,c) =
+    match occs with
+      | AllOccurrences ->
+        pr c
+      | NoOccurrences ->
+        failwith "pr_with_occurrences: no occurrences"
+      | OnlyOccurrences nl ->
+        hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++
+                 hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+      | AllOccurrencesBut nl ->
+        hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
+                 hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+
+  exception ComplexRedFlag
+
+  let pr_short_red_flag pr r =
+    if not r.rBeta ||  not r.rIota ||  not r.rZeta then raise ComplexRedFlag
+    else if List.is_empty r.rConst then
+      if r.rDelta then mt () else raise ComplexRedFlag
+    else (if r.rDelta then str "-" else mt ()) ++
+	   hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")
+
+  let pr_red_flag pr r =
+    try pr_short_red_flag pr r
+    with complexRedFlags ->
+      (if r.rBeta then pr_arg str "beta" else mt ()) ++
+	(if r.rIota then pr_arg str "iota" else mt ()) ++
+	(if r.rZeta then pr_arg str "zeta" else mt ()) ++
+	(if List.is_empty r.rConst then
+	   if r.rDelta then pr_arg str "delta"
+	   else mt ()
+	 else
+	   pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
+	     hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
+
+  let pr_union pr1 pr2 = function
+    | Inl a -> pr1 a
+    | Inr b -> pr2 b
+
+  let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
+    | Red false -> keyword "red"
+    | Hnf -> keyword "hnf"
+    | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
+		     ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
+    | Cbv f ->
+      if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then
+        keyword "compute"
+      else
+        hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f)
+    | Lazy f ->
+      hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f)
+    | Cbn f ->
+      hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f)
+    | Unfold l ->
+      hov 1 (keyword "unfold" ++ spc() ++
+               prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l)
+    | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l)
+    | Pattern l ->
+      hov 1 (keyword "pattern" ++
+               pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr)) l)
+
+    | Red true ->
+      error "Shouldn't be accessible from user."
+    | ExtraRedExpr s ->
+      str s
+    | CbvVm o ->
+      keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
+    | CbvNative o ->
+      keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
+
+  let pr_may_eval test prc prlc pr2 pr3 = function
+    | ConstrEval (r,c) ->
+      hov 0
+        (keyword "eval" ++ brk (1,1) ++
+           pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++
+           keyword "in" ++ spc() ++ prc c)
+    | ConstrContext ((_,id),c) ->
+      hov 0
+        (keyword "context" ++ spc () ++ pr_id id ++ spc () ++
+           str "[" ++ prlc c ++ str "]")
+    | ConstrTypeOf c ->
+      hov 1 (keyword "type of" ++ spc() ++ prc c)
+    | ConstrTerm c when test c ->
+      h 0 (str "(" ++ prc c ++ str ")")
+    | ConstrTerm c ->
+      prc c
+
+  let pr_may_eval a =
+    pr_may_eval (fun _ -> false) a
+
+  let pr_arg pr x = spc () ++ pr x
+
+  let pr_or_var pr = function
+    | ArgArg x -> pr x
+    | ArgVar (_,s) -> pr_id s
+
+  let pr_and_short_name pr (c,_) = pr c
+
+  let pr_or_by_notation f = function
+    | AN v -> f v
+    | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+
+  let pr_located pr (loc,x) = pr x
+
+  let pr_evaluable_reference = function
+    | EvalVarRef id -> pr_id id
+    | EvalConstRef sp -> pr_global (Globnames.ConstRef sp)
+
+  let pr_quantified_hypothesis = function
+    | AnonHyp n -> int n
+    | NamedHyp id -> pr_id id
+
+  let pr_binding prc = function
+    | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
+    | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+
+  let pr_bindings prc prlc = function
+    | ImplicitBindings l ->
+      brk (1,1) ++ keyword "with" ++ brk (1,1) ++
+        hv 0 (prlist_with_sep spc prc l)
+    | ExplicitBindings l ->
+      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 ()
+
+  let pr_bindings_no_with prc prlc = function
+    | ImplicitBindings l ->
+      brk (0,1) ++
+        prlist_with_sep spc prc l
+    | ExplicitBindings l ->
+      brk (0,1) ++
+        prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+    | NoBindings -> mt ()
+
+  let pr_clear_flag clear_flag pp x =
+    (match clear_flag with Some false -> str "!" | Some true -> str ">" | None -> mt())
+    ++ pp x
+
+  let pr_with_bindings prc prlc (c,bl) =
+    prc c ++ pr_bindings prc prlc bl
+
+  let pr_with_bindings_arg prc prlc (clear_flag,c) =
+    pr_clear_flag clear_flag (pr_with_bindings prc prlc) c
+
+  let pr_with_constr prc = function
+    | None -> mt ()
+    | Some c -> spc () ++ hov 1 (keyword "with" ++ spc () ++ prc c)
+
+  let pr_message_token prid = function
+    | MsgString s -> tag_string (qs s)
+    | MsgInt n -> int n
+    | MsgIdent id -> prid id
+
+  let pr_fresh_ids =
+    prlist (fun s -> spc() ++ pr_or_var (fun s -> tag_string (qs s)) s)
+
+  let with_evars ev s = if ev then "e" ^ s else s
+
+
+  let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
+    match Genarg.genarg_tag x with
+      | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
+      | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
+      | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
+      | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
+      | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
+      | ConstrMayEvalArgType ->
+        pr_may_eval prc prlc (pr_or_by_notation prref) prpat
+          (out_gen (rawwit wit_constr_may_eval) x)
+      | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x)
+      | RedExprArgType ->
+        pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
+          (out_gen (rawwit wit_red_expr) x)
+      | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
+      | ConstrWithBindingsArgType ->
+        pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x)
+      | BindingsArgType ->
+        pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x)
+      | ListArgType _ ->
+        let list_unpacker wit l =
+          let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
+          pr_sequence map (raw l)
+        in
+        hov 0 (list_unpack { list_unpacker } x)
+      | OptArgType _ ->
+        let opt_unpacker wit o = match raw o with
+          | None -> mt ()
+          | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x)
+        in
+        hov 0 (opt_unpack { opt_unpacker } x)
+      | PairArgType _ ->
+        let pair_unpacker wit1 wit2 o =
+          let p, q = raw o in
+          let p = in_gen (rawwit wit1) p in
+          let q = in_gen (rawwit wit2) q in
+          pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q]
+        in
+        hov 0 (pair_unpack { pair_unpacker } x)
+      | ExtraArgType s ->
+        try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x
+        with Not_found -> Genprint.generic_raw_print x
+
+
+  let rec pr_glb_generic prc prlc prtac prpat x =
+    match Genarg.genarg_tag x with
+      | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
+      | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
+      | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
+      | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
+      | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
+      | ConstrMayEvalArgType ->
+        pr_may_eval prc prlc
+          (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat
+          (out_gen (glbwit wit_constr_may_eval) x)
+      | QuantHypArgType ->
+        pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x)
+      | RedExprArgType ->
+        pr_red_expr
+          (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
+          (out_gen (glbwit wit_red_expr) x)
+      | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
+      | ConstrWithBindingsArgType ->
+        pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x)
+      | BindingsArgType ->
+        pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x)
+      | ListArgType _ ->
+        let list_unpacker wit l =
+          let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in
+          pr_sequence map (glb l)
+        in
+        hov 0 (list_unpack { list_unpacker } x)
+      | OptArgType _ ->
+        let opt_unpacker wit o = match glb o with
+          | None -> mt ()
+          | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x)
+        in
+        hov 0 (opt_unpack { opt_unpacker } x)
+      | PairArgType _ ->
+        let pair_unpacker wit1 wit2 o =
+          let p, q = glb o in
+          let p = in_gen (glbwit wit1) p in
+          let q = in_gen (glbwit wit2) q in
+          pr_sequence (pr_glb_generic prc prlc prtac prpat) [p; q]
+        in
+        hov 0 (pair_unpack { pair_unpacker } x)
+      | ExtraArgType s ->
+        try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x
+        with Not_found -> Genprint.generic_glb_print x
+
+  let rec pr_top_generic prc prlc prtac prpat x =
+    match Genarg.genarg_tag x with
+      | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
+      | IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
+      | VarArgType -> pr_id (out_gen (topwit wit_var) x)
+      | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
+      | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
+      | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
+      | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x)
+      | RedExprArgType ->
+        pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
+          (out_gen (topwit wit_red_expr) x)
+      | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
+      | ConstrWithBindingsArgType ->
+        let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in
+        pr_with_bindings prc prlc (c,b)
+      | BindingsArgType ->
+        pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it
+      | ListArgType _ ->
+        let list_unpacker wit l =
+          let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in
+          pr_sequence map (top l)
+        in
+        hov 0 (list_unpack { list_unpacker } x)
+      | OptArgType _ ->
+        let opt_unpacker wit o = match top o with
+          | None -> mt ()
+          | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x)
+        in
+        hov 0 (opt_unpack { opt_unpacker } x)
+      | PairArgType _ ->
+        let pair_unpacker wit1 wit2 o =
+          let p, q = top o in
+          let p = in_gen (topwit wit1) p in
+          let q = in_gen (topwit wit2) q in
+          pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q]
+        in
+        hov 0 (pair_unpack { pair_unpacker } x)
+      | ExtraArgType s ->
+        try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x
+        with Not_found -> Genprint.generic_top_print x
+
+  let rec tacarg_using_rule_token pr_gen = function
+    | Some s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al)
+    | None :: l, a :: al ->
+      let r = tacarg_using_rule_token pr_gen (l,al) in
+      pr_gen a :: r
+    | [], [] -> []
+    | _ -> failwith "Inconsistent arguments of extended tactic"
+
+  let pr_tacarg_using_rule pr_gen l =
+    let l = match l with
+    | (Some s :: l, al) ->
+      (** First terminal token should be considered as the name of the tactic,
+          so we tag it differently than the other terminal tokens. *)
+      primitive s :: (tacarg_using_rule_token pr_gen (l, al))
+    | _ -> tacarg_using_rule_token pr_gen l
+    in
+    pr_sequence (fun x -> x) l
+
+  let pr_extend_gen pr_gen lev s l =
+    try
+      let tags = List.map genarg_tag l in
+      let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
+      let p = pr_tacarg_using_rule pr_gen (pl,l) in
+      if lev' > lev then surround p else p
+    with Not_found ->
+      let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in
+      let args = match l with
+        | [] -> mt ()
+        | _ -> spc() ++ pr_sequence pr_gen l
+      in
+      str "<" ++ name ++ str ">" ++ args
+
+  let pr_alias_gen pr_gen lev key l =
+    try
+      let pp = KNmap.find key !prnotation_tab in
+      let (lev', pl) = pp.pptac_prods in
+      let p = pr_tacarg_using_rule pr_gen (pl, l) in
+      if lev' > lev then surround p else p
+    with Not_found ->
+      KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
+
+  let pr_raw_extend prc prlc prtac prpat =
+    pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
+  let pr_glob_extend prc prlc prtac prpat =
+    pr_extend_gen (pr_glb_generic prc prlc prtac prpat)
+  let pr_extend prc prlc prtac prpat =
+    pr_extend_gen (pr_top_generic prc prlc prtac prpat)
+
+  let pr_raw_alias prc prlc prtac prpat =
+    pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
+  let pr_glob_alias prc prlc prtac prpat =
+    pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
+  let pr_alias prc prlc prtac prpat =
+    pr_alias_gen (pr_top_generic prc prlc prtac prpat)
+
+  (**********************************************************************)
+  (* The tactic printer                                                 *)
+
+  let strip_prod_binders_expr n ty =
+    let rec strip_ty acc n ty =
+      match ty with
+          Constrexpr.CProdN(_,bll,a) ->
+            let nb =
+              List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
+            let bll = List.map (fun (x, _, y) -> x, y) bll in
+            if nb >= n then (List.rev (bll@acc)), a
+            else strip_ty (bll@acc) (n-nb) a
+        | _ -> error "Cannot translate fix tactic: not enough products" in
+    strip_ty [] n ty
+
+  let pr_ltac_or_var pr = function
+    | ArgArg x -> pr x
+    | ArgVar (loc,id) -> pr_with_comments loc (pr_id id)
+
+  let pr_ltac_constant kn =
+    if !Flags.in_debugger then pr_kn kn
+    else try
+           pr_qualid (Nametab.shortest_qualid_of_tactic kn)
+      with Not_found -> (* local tactic not accessible anymore *)
+        str "<" ++ pr_kn kn ++ str ">"
+
+  let pr_evaluable_reference_env env = function
+    | EvalVarRef id -> pr_id id
+    | EvalConstRef sp ->
+      Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp)
+
+  let pr_esubst prc l =
+    let pr_qhyp = function
+    (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
+      | (_,NamedHyp id,c) ->
+        str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
+    in
+    prlist_with_sep spc pr_qhyp l
+
+  let pr_bindings_gen for_ex prc prlc = function
+    | ImplicitBindings l ->
+      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 keyword "with" ++ spc ()) ++
+                 pr_esubst prlc l)
+    | NoBindings -> mt ()
+
+  let pr_bindings prc prlc = pr_bindings_gen false prc prlc
+
+  let pr_with_bindings prc prlc (c,bl) =
+    hov 1 (prc c ++ pr_bindings prc prlc bl)
+
+  let pr_as_disjunctive_ipat prc ipatl =
+    keyword "as" ++ spc () ++
+      pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
+
+  let pr_eqn_ipat (_,ipat) = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
+
+  let pr_with_induction_names prc = function
+    | None, None -> mt ()
+    | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat)
+    | None, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat prc ipat)
+    | Some eqpat, Some ipat ->
+      spc () ++
+        hov 1 (pr_as_disjunctive_ipat prc ipat ++ spc () ++ pr_eqn_ipat eqpat)
+
+  let pr_as_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 ()
+    | Some ipat -> pr_as_disjunctive_ipat prc ipat
+
+  let pr_as_ipat prc = function
+    | None -> mt ()
+    | Some ipat -> pr_as_intro_pattern prc ipat
+
+  let pr_as_name = function
+    | Anonymous -> mt ()
+    | 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
+
+  let pr_pose prc prlc na c = match na with
+    | Anonymous -> spc() ++ prc c
+    | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c)
+
+  let pr_assertion prc prdc _prlc ipat c = match ipat with
+    (* Use this "optimisation" or use only the general case ?
+       | IntroIdentifier id ->
+       spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
+    *)
+    | ipat ->
+      spc() ++ prc c ++ pr_as_ipat prdc ipat
+
+  let pr_assumption prc prdc prlc ipat c = match ipat with
+    (* Use this "optimisation" or use only the general case ?*)
+    (* it seems that this "optimisation" is somehow more natural *)
+    | Some (_,IntroNaming (IntroIdentifier id)) ->
+      spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c)
+    | ipat ->
+      spc() ++ prc c ++ pr_as_ipat prdc ipat
+
+  let pr_by_tactic prt = function
+    | TacId [] -> mt ()
+    | 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 "(" ++ keyword "type of" ++ spc () ++ pr_id id ++ str ")"
+      ) occs
+    | occs, InHypValueOnly ->
+      spc () ++ pr_with_occurrences (fun id ->
+        str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")"
+      ) occs
+
+  let pr_in pp = spc () ++ hov 0 (keyword "in" ++ pp)
+
+  let pr_simple_hyp_clause pr_id = function
+    | [] -> mt ()
+    | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
+
+  let pr_in_hyp_as prc pr_id = function
+    | None -> mt ()
+    | Some (clear,id,ipat) ->
+      pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat prc ipat
+
+  let pr_clauses default_is_concl pr_id = function
+    | { onhyps=Some []; concl_occs=occs }
+        when (match default_is_concl with Some true -> true | _ -> false) ->
+      pr_with_occurrences mt (occs,())
+    | { onhyps=None; concl_occs=AllOccurrences }
+        when (match default_is_concl with Some false -> true | _ -> false) -> mt ()
+    | { onhyps=None; concl_occs=NoOccurrences } ->
+      pr_in (str " * |-")
+    | { onhyps=None; concl_occs=occs } ->
+      pr_in (pr_with_occurrences (fun () -> str " *") (occs,()))
+    | { onhyps=Some l; concl_occs=occs } ->
+      let pr_occs = match occs with
+        | NoOccurrences -> mt ()
+        | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,())
+      in
+      pr_in
+        (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++ pr_occs)
+
+  let pr_orient b = if b then mt () else str "<- "
+
+  let pr_multi = function
+    | Precisely 1 -> mt ()
+    | Precisely n -> int n ++ str "!"
+    | UpTo n -> int n ++ str "?"
+    | RepeatStar -> str "?"
+    | RepeatPlus -> str "!"
+
+  let pr_induction_arg prc prlc = function
+    | ElimOnConstr c -> pr_with_bindings prc prlc c
+    | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
+    | ElimOnAnonHyp n -> int n
+
+  let pr_induction_kind = function
+    | SimpleInversion -> primitive "simple inversion"
+    | FullInversion -> primitive "inversion"
+    | FullInversionClear -> primitive "inversion_clear"
+
+  let pr_lazy = function
+    | General -> keyword "multi"
+    | Select -> keyword "lazy"
+    | Once -> 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. *)
+      keyword "context" ++ str" [" ++ pr_pat a ++ str "]"
+    | Subterm (b,Some id,a) ->
+      keyword "context" ++ spc () ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+
+  let pr_match_hyps pr_pat = function
+    | Hyp (nal,mp) ->
+      pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
+    | Def (nal,mv,mp) ->
+      pr_lname nal ++ str ":=" ++ pr_match_pattern pr_pat mv
+      ++ str ":" ++ pr_match_pattern pr_pat mp
+
+  let pr_match_rule m pr pr_pat = function
+    | Pat ([],mp,t) when m ->
+      pr_match_pattern pr_pat mp ++
+        spc () ++ str "=>" ++ brk (1,4) ++ pr t
+    (*
+      | Pat (rl,mp,t) ->
+      hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl ++
+      (if rl <> [] then spc () else mt ()) ++
+      hov 0 (str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+      str "=>" ++ brk (1,4) ++ pr t))
+    *)
+    | Pat (rl,mp,t) ->
+      hov 0 (
+        hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl) ++
+          (if not (List.is_empty rl) then spc () else mt ()) ++
+          hov 0 (
+            str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+              str "=>" ++ brk (1,4) ++ pr t))
+    | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
+
+  let pr_funvar = function
+    | None -> spc () ++ str "_"
+    | Some id -> spc () ++ pr_id id
+
+  let pr_let_clause k pr (id,(bl,t)) =
+    hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++
+             str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.ghost,t)))
+
+  let pr_let_clauses recflag pr = function
+    | hd::tl ->
+      hv 0
+        (pr_let_clause (if recflag then "let rec" else "let") pr hd ++
+           prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl)
+    | [] -> anomaly (Pp.str "LetIn must declare at least one binding")
+
+  let pr_seq_body pr tl =
+    hv 0 (str "[ " ++
+            prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
+            str " ]")
+
+  let pr_dispatch pr tl =
+    hv 0 (str "[>" ++
+            prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
+            str " ]")
+
+  let pr_opt_tactic pr = function
+    | TacId [] -> mt ()
+    | t -> pr t
+
+  let pr_tac_extend_gen pr tf tm tl =
+    prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++
+      pr_opt_tactic pr tm ++ str ".." ++
+      prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl
+
+  let pr_then_gen pr tf tm tl =
+    hv 0 (str "[ " ++
+            pr_tac_extend_gen pr tf tm tl ++
+            str " ]")
+
+  let pr_tac_extend pr tf tm tl =
+    hv 0 (str "[>" ++
+            pr_tac_extend_gen pr tf tm tl ++
+            str " ]")
+
+  let pr_hintbases = function
+    | None -> spc () ++ keyword "with" ++ str" *"
+    | Some [] -> mt ()
+    | Some l ->
+      spc () ++ hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
+
+  let pr_auto_using prc = function
+    | [] -> mt ()
+    | l -> spc () ++
+      hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
+
+  let string_of_debug = function
+    | Off -> ""
+    | Debug -> "debug "
+    | Info -> "info_"
+
+  let pr_then () = str ";"
+
+  let ltop = (5,E)
+  let lseq = 4
+  let ltactical = 3
+  let lorelse = 2
+  let llet = 5
+  let lfun = 5
+  let lcomplete = 1
+  let labstract = 3
+  let lmatch = 1
+  let latom = 0
+  let lcall = 1
+  let leval = 1
+  let ltatom = 1
+  let linfo = 5
+
+  let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
+
+  (** A printer for tactics that polymorphically works on the three
+      "raw", "glob" and "typed" levels *)
+
+  type 'a printer = {
+    pr_tactic    : tolerability -> 'tacexpr -> std_ppcmds;
+    pr_constr    : 'trm -> std_ppcmds;
+    pr_uconstr   : 'utrm -> std_ppcmds;
+    pr_lconstr   : 'trm -> std_ppcmds;
+    pr_dconstr   : 'dtrm -> std_ppcmds;
+    pr_pattern   : 'pat -> std_ppcmds;
+    pr_lpattern  : 'pat -> std_ppcmds;
+    pr_constant  : 'cst -> std_ppcmds;
+    pr_reference : 'ref -> std_ppcmds;
+    pr_name      : 'nam -> std_ppcmds;
+    pr_generic   : 'lev generic_argument -> std_ppcmds;
+    pr_extend    : int -> ml_tactic_name -> 'lev generic_argument list -> std_ppcmds;
+    pr_alias     : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds;
+  }
+
+  constraint 'a = <
+      term      :'trm;
+      utrm      :'utrm;
+      dterm     :'dtrm;
+      pattern   :'pat;
+      constant  :'cst;
+      reference :'ref;
+      name      :'nam;
+      tacexpr   :'tacexpr;
+      level     :'lev
+    >
+
+    let make_pr_tac pr strip_prod_binders tag_atom tag =
+
+        (* some shortcuts *)
+        let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in
+        let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in
+        let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
+        let pr_with_bindings_arg_full = pr_with_bindings_arg in
+        let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
+        let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
+
+        let pr_constrarg c = spc () ++ pr.pr_constr c in
+        let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
+        let pr_intarg n = spc () ++ int n in
+
+        (* Some printing combinators *)
+        let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in
+
+        let extract_binders = function
+          | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
+          | body -> ([],body) in
+
+        let pr_binder_fix (nal,t) =
+          (*  match t with
+              | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
+              | _ ->*)
+          let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
+          spc() ++ hov 1 (str"(" ++ s ++ str")") in
+
+        let pr_fix_tac (id,n,c) =
+          let rec set_nth_name avoid n = function
+          (nal,ty)::bll ->
+            if n <= List.length nal then
+              match List.chop (n-1) nal with
+                  _, (_,Name id) :: _ -> id, (nal,ty)::bll
+                | bef, (loc,Anonymous) :: aft ->
+                  let id = next_ident_away (Id.of_string"y") avoid in
+                  id, ((bef@(loc,Name id)::aft, ty)::bll)
+                | _ -> assert false
+            else
+              let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
+              (id,(nal,ty)::bll')
+            | [] -> assert false in
+          let (bll,ty) = strip_prod_binders n c in
+          let names =
+            List.fold_left
+              (fun ln (nal,_) -> List.fold_left
+                (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
+                ln nal)
+              [] bll in
+          let idarg,bll = set_nth_name names n bll in
+          let annot = match names with
+            | [_] ->
+              mt ()
+            | _ ->
+              spc() ++ str"{"
+              ++ keyword "struct" ++ spc ()
+              ++ pr_id idarg ++ str"}"
+          in
+          hov 1 (str"(" ++ pr_id id ++
+                   prlist pr_binder_fix bll ++ annot ++ str" :" ++
+                   pr_lconstrarg ty ++ str")") in
+        (*  spc() ++
+            hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+            c)
+        *)
+        let pr_cofix_tac (id,c) =
+          hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
+
+        (* Printing tactics as arguments *)
+        let rec pr_atom0 a = tag_atom a (match a with
+          | TacIntroPattern [] -> primitive "intros"
+          | TacIntroMove (None,MoveLast) -> primitive "intro"
+          | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ primitive "trivial"
+          | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ primitive "auto"
+          | TacClear (true,[]) -> primitive "clear"
+          | t -> str "(" ++ pr_atom1 t ++ str ")"
+        )
+
+        (* Main tactic printer *)
+        and pr_atom1 a = tag_atom a (match a with
+          (* Basic tactics *)
+          | TacIntroPattern [] as t ->
+            pr_atom0 t
+          | TacIntroPattern (_::_ as p) ->
+            hov 1 (primitive "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) ->
+            primitive "intro" ++ spc () ++ pr_id id
+          | TacIntroMove (ido,hto) ->
+            hov 1 (primitive "intro" ++ pr_opt pr_id ido ++
+                     Miscprint.pr_move_location pr.pr_name hto)
+          | TacExact c ->
+            hov 1 (primitive "exact" ++ pr_constrarg c)
+          | TacApply (a,ev,cb,inhyp) ->
+            hov 1 (
+              (if a then mt() else primitive "simple ") ++
+                primitive (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 (
+              primitive (with_evars ev "elim")
+              ++ pr_arg pr_with_bindings_arg cb
+              ++ pr_opt pr_eliminator cbo)
+          | TacCase (ev,cb) ->
+            hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
+          | TacFix (ido,n) -> hov 1 (primitive "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
+          | TacMutualFix (id,n,l) ->
+            hov 1 (
+              primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
+              ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l)
+          | TacCofix ido ->
+            hov 1 (primitive "cofix" ++ pr_opt pr_id ido)
+          | TacMutualCofix (id,l) ->
+            hov 1 (
+              primitive "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 (
+              primitive (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 (
+              primitive "pose proof"
+              ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
+            )
+          | TacGeneralize l ->
+            hov 1 (
+              primitive "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 (
+              primitive "generalize" ++ spc () ++ str "dependent"
+              ++ pr_constrarg c
+            )
+          | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
+            hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+          | TacLetTac (na,c,cl,b,e) ->
+            hov 1 (
+              (if b then primitive "set" else primitive "remember") ++
+                (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
+                 else pr_pose_as_style pr.pr_constr na c) ++
+                pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
+                pr_clauses (Some b) pr.pr_name cl)
+          (*  | TacInstantiate (n,c,ConclLocation ()) ->
+              hov 1 (str "instantiate" ++ spc() ++
+              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+              pr_lconstrarg c ++ str ")" ))
+              | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+              hov 1 (str "instantiate" ++ spc() ++
+              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+              pr_lconstrarg c ++ str ")" )
+              ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None)))
+          *)
+
+          (* Derived basic tactics *)
+          | TacInductionDestruct (isrec,ev,(l,el)) ->
+            hov 1 (
+              primitive (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 (
+              primitive "double induction"
+              ++ pr_arg pr_quantified_hypothesis h1
+              ++ pr_arg pr_quantified_hypothesis h2
+            )
+
+          (* Automation tactics *)
+          | TacTrivial (_,[],Some []) as x ->
+            pr_atom0 x
+          | TacTrivial (d,lems,db) ->
+            hov 0 (
+              str (string_of_debug d) ++ primitive "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) ++ primitive "auto"
+              ++ pr_opt (pr_or_var int) n
+              ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db
+            )
+
+          (* Context management *)
+          | TacClear (true,[]) as t ->
+            pr_atom0 t
+          | TacClear (keep,l) ->
+            hov 1 (
+              primitive "clear" ++ spc ()
+              ++ (if keep then str "- " else mt ())
+              ++ prlist_with_sep spc pr.pr_name l
+            )
+          | TacClearBody l ->
+            hov 1 (
+              primitive "clearbody" ++ spc ()
+              ++ prlist_with_sep spc pr.pr_name l
+            )
+          | TacMove (id1,id2) ->
+            hov 1 (
+              primitive "move"
+              ++ brk (1,1) ++ pr.pr_name id1
+              ++ Miscprint.pr_move_location pr.pr_name id2
+            )
+          | TacRename l ->
+            hov 1 (
+              primitive "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 (
+              primitive (with_evars ev "exists")
+              ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l
+            )
+
+          (* Conversion *)
+          | TacReduce (r,h) ->
+            hov 1 (
+              pr_red_expr r
+              ++ pr_clauses (Some true) pr.pr_name h
+            )
+          | TacChange (op,c,h) ->
+            hov 1 (
+              primitive "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 ->
+            primitive "symmetry" ++ pr_clauses (Some true) pr.pr_name cls
+
+          (* Equality and inversion *)
+          | TacRewrite (ev,l,cl,by) ->
+            hov 1 (
+              primitive (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 (
+              primitive "dependent " ++ pr_induction_kind k ++ spc ()
+              ++ pr_quantified_hypothesis hyp
+              ++ pr_with_inversion_names pr.pr_dconstr ids
+              ++ pr_with_constr pr.pr_constr c
+            )
+          | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
+            hov 1 (
+              pr_induction_kind k ++ spc ()
+              ++ pr_quantified_hypothesis hyp
+              ++ pr_with_inversion_names pr.pr_dconstr ids
+              ++ pr_simple_hyp_clause pr.pr_name cl
+            )
+          | TacInversion (InversionUsing (c,cl),hyp) ->
+            hov 1 (
+              primitive "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 return (doc, l) = (tag tac doc, l) in
+          let (strm, prec) = return (match tac with
+            | TacAbstract (t,None) ->
+              keyword "abstract " ++ pr_tac (labstract,L) t, labstract
+            | TacAbstract (t,Some 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
+                  ++ spc () ++ keyword "in"
+                 ) ++ fnl () ++ pr_tac (llet,E) u),
+              llet
+            | TacMatch (lz,t,lrul) ->
+              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
+                ++ 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 (
+                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),
+              lseq
+            | TacThen (t1,t2) ->
+              hov 1 (
+                pr_tac (lseq,E) t1 ++ pr_then () ++ spc ()
+                ++ pr_tac (lseq,L) t2),
+              lseq
+            | TacDispatch tl ->
+              pr_dispatch (pr_tac ltop) tl, lseq
+            | TacExtendTac (tf,t,tr) ->
+              pr_tac_extend (pr_tac ltop) tf t tr , lseq
+            | TacThens3parts (t1,tf,t2,tl) ->
+              hov 1 (
+                pr_tac (lseq,E) t1 ++ pr_then () ++ spc ()
+                ++ pr_then_gen (pr_tac ltop) tf t2 tl),
+              lseq
+            | TacTry t ->
+              hov 1 (
+                keyword "try" ++ spc () ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacDo (n,t) ->
+              hov 1 (
+                str "do" ++ spc ()
+                ++ pr_or_var int n ++ spc ()
+                ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacTimeout (n,t) ->
+              hov 1 (
+                keyword "timeout "
+                ++ pr_or_var int n ++ spc ()
+                ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacTime (s,t) ->
+              hov 1 (
+                keyword "time"
+                ++ pr_opt str s ++ spc ()
+                ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacRepeat t ->
+              hov 1 (
+                keyword "repeat" ++ spc ()
+                ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacProgress t ->
+              hov 1 (
+                keyword "progress" ++ spc ()
+                ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacShowHyps t ->
+              hov 1 (
+                keyword "infoH" ++ spc ()
+                ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacInfo t ->
+              hov 1 (
+                keyword "info" ++ spc ()
+                ++ pr_tac (ltactical,E) t),
+              linfo
+            | TacOr (t1,t2) ->
+              hov 1 (
+                pr_tac (lorelse,L) t1 ++ spc ()
+                ++ str "+" ++ brk (1,1)
+                ++ pr_tac (lorelse,E) t2),
+              lorelse
+            | TacOnce t ->
+              hov 1 (
+                keyword "once" ++ spc ()
+                ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacExactlyOnce t ->
+              hov 1 (
+                keyword "exactly_once" ++ spc ()
+                ++ pr_tac (ltactical,E) t),
+              ltactical
+            | TacIfThenCatch (t,tt,te) ->
+                hov 1 (
+                 str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++
+                 str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++
+                 str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)),
+                ltactical
+            | TacOrelse (t1,t2) ->
+              hov 1 (
+                pr_tac (lorelse,L) t1 ++ spc ()
+                ++ str "||" ++ brk (1,1)
+                ++ pr_tac (lorelse,E) t2),
+              lorelse
+            | TacFail (g,n,l) ->
+              let arg =
+                match n with
+                  | ArgArg 0 -> mt ()
+                  | _ -> pr_arg (pr_or_var int) n
+              in
+              let name =
+                match g with
+                | TacGlobal -> keyword "gfail"
+                | TacLocal -> keyword "fail"
+              in
+              hov 1 (
+                name ++ arg
+                ++ prlist (pr_arg (pr_message_token pr.pr_name)) l),
+              latom
+            | TacFirst tl ->
+              keyword "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
+            | TacSolve tl ->
+              keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
+            | TacComplete t ->
+              pr_tac (lcomplete,E) t, lcomplete
+            | TacId l ->
+              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(_,ConstrMayEval (ConstrTerm c)) ->
+              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) ->
+              primitive "fresh" ++ pr_fresh_ids l, latom
+            | TacArg(_,TacGeneric arg) ->
+              pr.pr_generic arg, latom
+            | TacArg(_,TacCall(loc,f,[])) ->
+              pr.pr_reference f, latom
+            | TacArg(_,TacCall(loc,f,l)) ->
+              pr_with_comments loc (hov 1 (
+                pr.pr_reference f ++ spc ()
+                ++ prlist_with_sep spc pr_tacarg l)),
+              lcall
+            | TacArg (_,a) ->
+              pr_tacarg a, latom
+            | TacML (loc,s,l) ->
+              pr_with_comments loc (pr.pr_extend 1 s l), lcall
+            | TacAlias (loc,kn,l) ->
+              pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom
+          )
+          in
+          if prec_less prec inherited then strm
+          else str"(" ++ strm ++ str")"
+
+        and pr_tacarg = function
+          | TacDynamic (loc,t) ->
+            pr_with_comments loc (
+              str "<" ++ 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 ->
+            keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
+
+        in pr_tac
+
+  let strip_prod_binders_glob_constr n (ty,_) =
+    let rec strip_ty acc n ty =
+      if Int.equal n 0 then (List.rev acc, (ty,None)) else
+        match ty with
+            Glob_term.GProd(loc,na,Explicit,a,b) ->
+              strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b
+          | _ -> error "Cannot translate fix tactic: not enough products" in
+    strip_ty [] n ty
+
+  let raw_printers =
+    (strip_prod_binders_expr)
+
+  let rec pr_raw_tactic_level n (t:raw_tactic_expr) =
+    let pr = {
+      pr_tactic = pr_raw_tactic_level;
+      pr_constr = pr_constr_expr;
+      pr_uconstr = pr_constr_expr;
+      pr_dconstr = pr_constr_expr;
+      pr_lconstr = pr_lconstr_expr;
+      pr_pattern = pr_constr_pattern_expr;
+      pr_lpattern = pr_lconstr_pattern_expr;
+      pr_constant = pr_or_by_notation pr_reference;
+      pr_reference = pr_reference;
+      pr_name = pr_lident;
+      pr_generic = Genprint.generic_raw_print;
+      pr_extend = pr_raw_extend pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
+      pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
+    } in
+    make_pr_tac
+      pr raw_printers
+      tag_raw_atomic_tactic_expr tag_raw_tactic_expr
+      n t
+
+  let pr_raw_tactic = pr_raw_tactic_level ltop
+
+  let pr_and_constr_expr pr (c,_) = pr c
+
+  let pr_pat_and_constr_expr pr ((c,_),_) = pr c
+
+  let rec pr_glob_tactic_level env n t =
+    let glob_printers =
+      (strip_prod_binders_glob_constr)
+    in
+    let rec prtac n (t:glob_tactic_expr) =
+      let pr = {
+        pr_tactic = prtac;
+        pr_constr = pr_and_constr_expr (pr_glob_constr_env env);
+        pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env);
+        pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
+        pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env);
+        pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
+        pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
+        pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
+        pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
+        pr_name = pr_lident;
+        pr_generic = Genprint.generic_glb_print;
+        pr_extend = pr_glob_extend
+          (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+          prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
+        pr_alias = pr_glob_alias
+          (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+          prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
+      } in
+      make_pr_tac
+        pr glob_printers
+        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
+        match Term.kind_of_term ty with
+            Term.Prod(na,a,b) ->
+              strip_ty (([Loc.ghost,na],a)::acc) (n-1) b
+          | _ -> error "Cannot translate fix tactic: not enough products" in
+    strip_ty [] n ty
+
+  let pr_tactic_level env n t =
+    let typed_printers =
+      (strip_prod_binders_constr)
+    in
+    let prtac n (t:tactic_expr) =
+      let pr = {
+        pr_tactic = pr_glob_tactic_level env;
+        pr_constr = pr_constr_env env Evd.empty;
+        pr_uconstr = pr_closed_glob_env env Evd.empty;
+        pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
+        pr_lconstr = pr_lconstr_env env Evd.empty;
+        pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
+        pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
+        pr_constant = pr_and_short_name (pr_evaluable_reference_env env);
+        pr_reference = pr_located pr_ltac_constant;
+        pr_name = pr_id;
+        pr_generic = Genprint.generic_top_print;
+        pr_extend = pr_extend
+          (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
+          (pr_glob_tactic_level env) pr_constr_pattern;
+        pr_alias = pr_alias
+          (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
+          (pr_glob_tactic_level env) pr_constr_pattern;
+      }
+      in
+      make_pr_tac
+        pr typed_printers
+        tag_atomic_tactic_expr tag_tactic_expr
+        n t
+    in
+    prtac n t
+
+  let pr_tactic env = pr_tactic_level env ltop
+
+end
+
+module Tag =
+struct
+  let keyword =
+    let style = Terminal.make ~bold:true () in
+    Ppstyle.make ~style ["tactic"; "keyword"]
+
+  let primitive =
+    let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
+    Ppstyle.make ~style ["tactic"; "primitive"]
+
+  let string =
+    let style = Terminal.make ~fg_color:`LIGHT_RED () in
+    Ppstyle.make ~style ["tactic"; "string"]
+
+end
+
+include Make (Ppconstr) (struct
+    let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
+    let do_not_tag _ x = x
+    let tag_keyword                 = tag Tag.keyword
+    let tag_primitive               = tag Tag.primitive
+    let tag_string                  = tag Tag.string
+    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 *)
+
+let () =
+  let pr_bool b = if b then str "true" else str "false" in
+  let pr_unit _ = str "()" in
+  let pr_string s = str "\"" ++ str s ++ str "\"" in
+  Genprint.register_print0 Constrarg.wit_ref
+    pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+  Genprint.register_print0
+    Constrarg.wit_intro_pattern
+    (Miscprint.pr_intro_pattern pr_constr_expr)
+    (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
+    (Miscprint.pr_intro_pattern (fun c -> pr_constr (snd (c (Global.env()) Evd.empty))));
+  Genprint.register_print0
+    Constrarg.wit_clause_dft_concl
+    (pr_clauses (Some true) pr_lident)
+    (pr_clauses (Some true) pr_lident)
+    (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
+  ;
+  Genprint.register_print0 Constrarg.wit_sort
+    pr_glob_sort pr_glob_sort (pr_sort Evd.empty);
+  Genprint.register_print0
+    Constrarg.wit_uconstr
+    Ppconstr.pr_constr_expr
+    (fun (c,_) -> Printer.pr_glob_constr c)
+    Printer.pr_closed_glob
+  ;
+  Genprint.register_print0 Stdarg.wit_int int int int;
+  Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
+  Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
+  Genprint.register_print0 Stdarg.wit_pre_ident str str str;
+  Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string
+
+let () =
+  let printer _ _ prtac = prtac (0, E) in
+  declare_extra_genarg_pprule wit_tactic printer printer printer
+
+let _ = Hook.set Tactic_debug.tactic_printer
+  (fun x -> pr_glob_tactic (Global.env()) x)
+
+let _ = Hook.set Tactic_debug.match_pattern_printer
+  (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp)
+
+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 = struct
+
+  include Make (Ppconstr.Richpp) (struct
+    open Ppannotation
+    let do_not_tag _ x = x
+    let tag e s = Pp.tag (Pp.Tag.inj e tag) s
+    let tag_keyword                   = tag AKeyword
+    let tag_primitive                 = tag AKeyword
+    let tag_string                    = do_not_tag ()
+    let tag_glob_tactic_expr        e = tag (AGlobTacticExpr e)
+    let tag_glob_atomic_tactic_expr a = tag (AGlobAtomicTacticExpr a)
+    let tag_raw_tactic_expr         e = tag (ARawTacticExpr e)
+    let tag_raw_atomic_tactic_expr  a = tag (ARawAtomicTacticExpr a)
+    let tag_tactic_expr             e = tag (ATacticExpr e)
+    let tag_atomic_tactic_expr      a = tag (AAtomicTacticExpr a)
+  end)
+
+end
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
new file mode 100644
index 00000000..284237f0
--- /dev/null
+++ b/printing/pptactic.mli
@@ -0,0 +1,65 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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}. *)
+module Richpp : Pptacticsig.Pp
+
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
new file mode 100644
index 00000000..98b5757d
--- /dev/null
+++ b/printing/pptacticsig.mli
@@ -0,0 +1,95 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Genarg
+open Names
+open Constrexpr
+open Tacexpr
+open Ppextend
+open Environ
+open Pattern
+open Misctypes
+
+module type Pp = sig
+
+  val pr_with_occurrences :
+    ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds
+  val pr_red_expr :
+    ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
+    ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds
+  val pr_may_eval :
+    ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+    ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
+
+  val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+  val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
+  val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
+
+  val pr_clauses :  bool option ->
+    ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+  val pr_raw_generic :
+    (constr_expr -> std_ppcmds) ->
+    (constr_expr -> std_ppcmds) ->
+    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+    (constr_expr -> std_ppcmds) ->
+    (Libnames.reference -> std_ppcmds) -> rlevel generic_argument ->
+    std_ppcmds
+
+  val pr_glb_generic :
+    (glob_constr_and_expr -> Pp.std_ppcmds) ->
+    (glob_constr_and_expr -> Pp.std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    (glob_constr_pattern_and_expr -> std_ppcmds) ->
+    glevel generic_argument -> std_ppcmds
+
+  val pr_top_generic :
+    (Term.constr -> std_ppcmds) ->
+    (Term.constr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    (Pattern.constr_pattern -> std_ppcmds) ->
+    tlevel generic_argument ->
+    std_ppcmds
+
+  val pr_raw_extend:
+    (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
+    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+    (constr_expr -> std_ppcmds) -> int ->
+    ml_tactic_name -> raw_generic_argument list -> std_ppcmds
+
+  val pr_glob_extend:
+    (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    (glob_constr_pattern_and_expr -> std_ppcmds) -> int ->
+    ml_tactic_name -> glob_generic_argument list -> std_ppcmds
+
+  val pr_extend :
+    (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+    (constr_pattern -> std_ppcmds) -> int ->
+    ml_tactic_name -> typed_generic_argument list -> std_ppcmds
+
+  val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
+
+  val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
+
+  val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
+
+  val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
+
+  val pr_tactic : env -> tactic_expr -> std_ppcmds
+
+  val pr_hintbases : string list option -> std_ppcmds
+
+  val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
+
+  val pr_bindings :
+    ('constr -> std_ppcmds) ->
+    ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
+
+end
diff --git a/printing/pputils.ml b/printing/pputils.ml
new file mode 100644
index 00000000..ee1a39ef
--- /dev/null
+++ b/printing/pputils.ml
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+
+let pr_located pr (loc, x) =
+  if Flags.do_beautify () && loc <> Loc.ghost then
+    let (b, e) = Loc.unloc loc in
+    Pp.comment b ++ pr x ++ Pp.comment e
+  else pr x
diff --git a/printing/pputils.mli b/printing/pputils.mli
new file mode 100644
index 00000000..72877483
--- /dev/null
+++ b/printing/pputils.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+
+val pr_located : ('a -> std_ppcmds) -> 'a Loc.located -> std_ppcmds
+(** Prints an object surrounded by its commented location *)
+
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
new file mode 100644
index 00000000..e9e335ec
--- /dev/null
+++ b/printing/ppvernac.ml
@@ -0,0 +1,1296 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+
+open Errors
+open Util
+open Extend
+open Vernacexpr
+open Pputils
+open Libnames
+open Constrexpr
+open Constrexpr_ops
+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
+  end)
+= struct
+
+  open Taggers
+  open Ppconstr
+  open Pptactic
+
+  let keyword s = tag_keyword (str s)
+
+  let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
+
+  let pr_lident (loc,id) =
+    if Loc.is_ghost loc then
+      let (b,_) = Loc.unloc loc in
+      pr_located pr_id (Loc.make_loc (b,b + String.length(Id.to_string id)),id)
+    else
+      pr_id id
+
+  let string_of_fqid fqid =
+    String.concat "." (List.map Id.to_string fqid)
+
+  let pr_fqid fqid = str (string_of_fqid fqid)
+
+  let pr_lfqid (loc,fqid) =
+    if Loc.is_ghost loc then
+      let (b,_) = Loc.unloc loc in
+      pr_located pr_fqid (Loc.make_loc (b,b + String.length(string_of_fqid fqid)),fqid)
+    else
+      pr_fqid fqid
+
+  let pr_lname = function
+    | (loc,Name id) -> pr_lident (loc,id)
+    | lna -> pr_located pr_name lna
+
+  let pr_smart_global = pr_or_by_notation pr_reference
+
+  let pr_ltac_ref = Libnames.pr_reference
+
+  let pr_module = Libnames.pr_reference
+
+  let pr_import_module = Libnames.pr_reference
+
+  let sep_end = function
+    | VernacBullet _
+    | VernacSubproof None
+    | VernacEndSubproof -> str""
+    | _ -> str"."
+
+  let pr_gen t =
+    pr_raw_generic
+      pr_constr_expr
+      pr_lconstr_expr
+      pr_raw_tactic_level
+      pr_constr_expr
+      pr_reference t
+
+  let sep = fun _ -> spc()
+  let sep_v2 = fun _ -> str"," ++ spc()
+
+  let pr_ne_sep sep pr = function
+  [] -> mt()
+    | l -> sep() ++ pr l
+
+  let pr_set_entry_type = function
+    | ETName -> str"ident"
+    | ETReference -> str"global"
+    | ETPattern -> str"pattern"
+    | ETConstr _ -> str"constr"
+    | ETOther (_,e) -> str e
+    | ETBigint -> str "bigint"
+    | ETBinder true -> str "binder"
+    | ETBinder false -> str "closed binder"
+    | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type"
+
+  let strip_meta id =
+    let s = Id.to_string id in
+    if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1))
+    else id
+
+  let pr_production_item = function
+    | TacNonTerm (loc,nt,Some (p,sep)) ->
+      let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in
+      str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")"
+    | TacNonTerm (loc,nt,None) -> str nt
+    | TacTerm s -> qs s
+
+  let pr_comment pr_c = function
+    | CommentConstr c -> pr_c c
+    | CommentString s -> qs s
+    | CommentInt n -> int n
+
+  let pr_in_out_modules = function
+    | SearchInside l -> spc() ++ keyword "inside" ++ spc() ++ prlist_with_sep sep pr_module l
+    | SearchOutside [] -> mt()
+    | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l
+
+  let pr_search_about (b,c) =
+    (if b then str "-" else mt()) ++
+      match c with
+        | SearchSubPattern p -> pr_constr_pattern_expr p
+        | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+
+  let pr_search a gopt b pr_p =
+    pr_opt (fun g -> int g ++ str ":"++ spc()) gopt
+    ++
+      match a with
+      | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+      | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+      | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
+      | SearchAbout sl ->
+	 keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
+
+  let pr_locality local = if local then keyword "Local" else keyword "Global"
+
+  let pr_explanation (e,b,f) =
+    let a = match e with
+      | ExplByPos (n,_) -> anomaly (Pp.str "No more supported")
+      | ExplByName id -> pr_id id in
+    let a = if f then str"!" ++ a else a in
+    if b then str "[" ++ a ++ str "]" else a
+
+  let pr_option_ref_value = function
+    | QualidRefValue id -> pr_reference id
+    | StringRefValue s -> qs s
+
+  let pr_printoption table b =
+    prlist_with_sep spc str table ++
+      pr_opt (prlist_with_sep sep pr_option_ref_value) b
+
+  let pr_set_option a b =
+    let pr_opt_value = function
+      | IntValue None -> assert false
+    (* This should not happen because of the grammar *)
+      | IntValue (Some n) -> spc() ++ int n
+      | StringValue s -> spc() ++ str s
+      | BoolValue b -> mt()
+    in pr_printoption a None ++ pr_opt_value b
+
+  let pr_topcmd _ = str"(* <Warning> : No printer for toplevel commands *)"
+
+  let pr_opt_hintbases l = match l with
+    | [] -> mt()
+    | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
+
+  let pr_reference_or_constr pr_c = function
+    | HintsReference r -> pr_reference r
+    | HintsConstr c -> pr_c c
+
+  let pr_hints db h pr_c pr_pat =
+    let opth = pr_opt_hintbases db  in
+    let pph =
+      match h with
+        | HintsResolve l ->
+          keyword "Resolve " ++ prlist_with_sep sep
+            (fun (pri, _, c) -> pr_reference_or_constr pr_c c ++
+              match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
+            l
+        | HintsImmediate l ->
+          keyword "Immediate" ++ spc() ++
+            prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l
+        | HintsUnfold l ->
+          keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_reference l
+        | HintsTransparency (l, b) ->
+          keyword (if b then "Transparent" else "Opaque")
+          ++ spc ()
+          ++ prlist_with_sep sep pr_reference l
+        | HintsMode (m, l) ->
+          keyword "Mode"
+          ++ spc ()
+          ++ pr_reference m ++ spc() ++ prlist_with_sep spc
+            (fun b -> if b then str"+" else str"-") l
+        | HintsConstructors c ->
+          keyword "Constructors"
+          ++ spc() ++ prlist_with_sep spc pr_reference c
+        | HintsExtern (n,c,tac) ->
+          let pat = match c with None -> mt () | Some pat -> pr_pat pat in
+          keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
+            spc() ++ pr_raw_tactic tac
+    in
+    hov 2 (keyword "Hint "++ pph ++ opth)
+
+  let pr_with_declaration pr_c = function
+    | CWith_Definition (id,c) ->
+      let p = pr_c c in
+      keyword "Definition" ++ spc() ++ pr_lfqid id ++ str" := " ++ p
+    | CWith_Module (id,qid) ->
+      keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
+        pr_located pr_qualid qid
+
+  let rec pr_module_ast leading_space pr_c = function
+    | CMident qid ->
+      if leading_space then
+        spc () ++ pr_located pr_qualid qid
+      else
+        pr_located pr_qualid qid
+    | CMwith (_,mty,decl) ->
+      let m = pr_module_ast leading_space pr_c mty in
+      let p = pr_with_declaration pr_c decl in
+      m ++ spc() ++ keyword "with" ++ spc() ++ p
+    | CMapply (_,me1,(CMident _ as me2)) ->
+      pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2
+    | CMapply (_,me1,me2) ->
+      pr_module_ast leading_space pr_c me1 ++ spc() ++
+        hov 1 (str"(" ++ pr_module_ast false pr_c me2 ++ str")")
+
+  let pr_inline = function
+    | DefaultInline -> mt ()
+    | NoInline -> str "[no inline]"
+    | InlineAt i -> str "[inline at level " ++ int i ++ str "]"
+
+  let pr_module_ast_inl leading_space pr_c (mast,inl) =
+    pr_module_ast leading_space pr_c mast ++ pr_inline inl
+
+  let pr_of_module_type prc = function
+    | Enforce mty -> str ":" ++ pr_module_ast_inl true prc mty
+    | Check mtys ->
+      prlist_strict (fun m -> str "<:" ++ pr_module_ast_inl true prc m) mtys
+
+  let pr_require_token = function
+    | Some true ->
+      keyword "Export" ++ spc ()
+    | Some false ->
+      keyword "Import" ++ spc ()
+    | None -> mt()
+
+  let pr_module_vardecls pr_c (export,idl,(mty,inl)) =
+    let m = pr_module_ast true pr_c mty in
+    spc() ++
+      hov 1 (str"(" ++ pr_require_token export ++
+               prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
+
+  let pr_module_binders l pr_c =
+    prlist_strict (pr_module_vardecls pr_c) l
+
+  let pr_type_option pr_c = function
+    | CHole (loc, k, Misctypes.IntroAnonymous, _) -> mt()
+    | _ as c -> brk(0,2) ++ str" :" ++ pr_c c
+
+  let pr_decl_notation prc ((loc,ntn),c,scopt) =
+    fnl () ++ keyword "where " ++ qs ntn ++ str " := " ++ prc c ++
+      pr_opt (fun sc -> str ": " ++ str sc) scopt
+
+  let pr_binders_arg =
+    pr_ne_sep spc pr_binders
+
+  let pr_and_type_binders_arg bl =
+    pr_binders_arg bl
+
+  let pr_onescheme (idop,schem) =
+    match schem with
+      | InductionScheme (dep,ind,s) ->
+        (match idop with
+          | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+          | None -> spc ()
+        ) ++
+          hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for")
+                 ++ spc() ++ pr_smart_global ind) ++ spc() ++
+          hov 0 (keyword "Sort" ++ spc() ++ pr_glob_sort s)
+      | CaseScheme (dep,ind,s) ->
+        (match idop with
+          | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+          | None -> spc ()
+        ) ++
+          hov 0 ((if dep then keyword "Elimination for" else keyword "Case for")
+                 ++ spc() ++ pr_smart_global ind) ++ spc() ++
+          hov 0 (keyword "Sort" ++ spc() ++ pr_glob_sort s)
+      | EqualityScheme ind ->
+        (match idop with
+          | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+          | None -> spc()
+        ) ++
+          hov 0 (keyword "Equality for")
+        ++ spc() ++ pr_smart_global ind
+
+  let begin_of_inductive = function
+    | [] -> 0
+    | (_,((loc,_),_))::_ -> fst (Loc.unloc loc)
+
+  let pr_class_rawexpr = function
+    | FunClass -> keyword "Funclass"
+    | SortClass -> keyword "Sortclass"
+    | RefClass qid -> pr_smart_global qid
+
+  let pr_assumption_token many (l,a) =
+    let l = match l with Some x -> x | None -> Decl_kinds.Global in
+    match l, a with
+      | (Discharge,Logical) ->
+        keyword (if many then "Hypotheses" else "Hypothesis")
+      | (Discharge,Definitional) ->
+        keyword (if many then "Variables" else "Variable")
+      | (Global,Logical) ->
+        keyword (if many then "Axioms" else "Axiom")
+      | (Global,Definitional) ->
+        keyword (if many then "Parameters" else "Parameter")
+      | (Local, Logical) ->
+        keyword (if many then "Local Axioms" else "Local Axiom")
+      | (Local,Definitional) ->
+        keyword (if many then "Local Parameters" else "Local Parameter")
+      | (Global,Conjectural) -> str"Conjecture"
+      | ((Discharge | Local),Conjectural) ->
+        anomaly (Pp.str "Don't know how to beautify a local conjecture")
+
+  let pr_params pr_c (xl,(c,t)) =
+    hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
+             (if c then str":>" else str":" ++
+                 spc() ++ pr_c t))
+
+  let rec factorize = function
+    | [] -> []
+    | (c,(idl,t))::l ->
+      match factorize l with
+        | (xl,((c', t') as r))::l'
+            when (c : bool) == c' && Pervasives.(=) t t' ->
+          (** FIXME: we need equality on constr_expr *)
+          (idl@xl,r)::l'
+        | l' -> (idl,(c,t))::l'
+
+  let pr_ne_params_list pr_c l =
+    match factorize l with
+      | [p] -> pr_params pr_c p
+      | l ->
+        prlist_with_sep spc
+          (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
+(*
+  prlist_with_sep pr_semicolon (pr_params pr_c)
+*)
+
+  let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
+
+  let pr_syntax_modifier = function
+    | SetItemLevel (l,NextLevel) ->
+      prlist_with_sep sep_v2 str l ++
+        spc() ++ keyword "at next level"
+    | SetItemLevel (l,NumLevel n) ->
+      prlist_with_sep sep_v2 str l ++
+        spc() ++ keyword "at level" ++ spc() ++ int n
+    | SetLevel n -> keyword "at level" ++ spc() ++ int n
+    | SetAssoc LeftA -> keyword "left associativity"
+    | SetAssoc RightA -> keyword "right associativity"
+    | SetAssoc NonA -> keyword "no associativity"
+    | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
+    | SetOnlyParsing Flags.Current -> keyword "only parsing"
+    | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
+    | SetFormat("text",s) -> keyword "format " ++ pr_located qs s
+    | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s
+
+  let pr_syntax_modifiers = function
+    | [] -> mt()
+    | l -> spc() ++
+      hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
+
+  let print_level n =
+    if not (Int.equal n 0) then
+      spc () ++ tag_keyword (str "(at level " ++ int n ++ str ")")
+    else
+      mt ()
+
+  let pr_grammar_tactic_rule n (_,pil,t) =
+    hov 2 (keyword "Tactic Notation" ++ print_level n ++ spc() ++
+             hov 0 (prlist_with_sep sep pr_production_item pil ++
+                      spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
+
+  let pr_statement head (id,(bl,c,guard)) =
+    assert (not (Option.is_empty id));
+    hov 2
+      (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
+         (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
+         pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
+         str":" ++ pr_spc_lconstr c)
+
+  let pr_priority = function
+    | None -> mt ()
+    | Some i -> spc () ++ str "|" ++ spc () ++ int i
+
+(**************************************)
+(* Pretty printer for vernac commands *)
+(**************************************)
+  let make_pr_vernac pr_constr pr_lconstr =
+    let pr_constrarg c = spc () ++ pr_constr c in
+    let pr_lconstrarg c = spc () ++ pr_lconstr c in
+    let pr_intarg n = spc () ++ int n in
+    let pr_oc = function
+    None -> str" :"
+      | Some true -> str" :>"
+      | Some false -> str" :>>"
+    in
+    let pr_record_field ((x, pri), ntn) =
+      let prx = match x with
+        | (oc,AssumExpr (id,t)) ->
+          hov 1 (pr_lname id ++
+                   pr_oc oc ++ spc() ++
+                   pr_lconstr_expr t)
+        | (oc,DefExpr(id,b,opt)) -> (match opt with
+            | Some t ->
+              hov 1 (pr_lname id ++
+                       pr_oc oc ++ spc() ++
+                       pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
+            | None ->
+              hov 1 (pr_lname id ++ str" :=" ++ spc() ++
+                       pr_lconstr b)) in
+      let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
+      prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn
+    in
+    let pr_record_decl b c fs =
+      pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
+        hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
+    in
+
+    let pr_printable = function
+      | PrintFullContext ->
+        keyword "Print All"
+      | PrintSectionContext s ->
+        keyword "Print Section" ++ spc() ++ Libnames.pr_reference s
+      | PrintGrammar ent ->
+        keyword "Print Grammar" ++ spc() ++ str ent
+      | PrintLoadPath dir ->
+        keyword "Print LoadPath" ++ pr_opt pr_dirpath dir
+      | PrintModules ->
+        keyword "Print Modules"
+      | PrintMLLoadPath ->
+        keyword "Print ML Path"
+      | PrintMLModules ->
+        keyword "Print ML Modules"
+      | PrintDebugGC ->
+        keyword "Print ML GC"
+      | PrintGraph ->
+        keyword "Print Graph"
+      | PrintClasses ->
+        keyword "Print Classes"
+      | PrintTypeClasses ->
+        keyword "Print TypeClasses"
+      | PrintInstances qid ->
+        keyword "Print Instances" ++ spc () ++ pr_smart_global qid
+      | PrintLtac qid ->
+        keyword "Print Ltac" ++ spc() ++ pr_ltac_ref qid
+      | PrintCoercions ->
+        keyword "Print Coercions"
+      | PrintCoercionPaths (s,t) ->
+        keyword "Print Coercion Paths" ++ spc()
+        ++ pr_class_rawexpr s ++ spc()
+        ++ pr_class_rawexpr t
+      | PrintCanonicalConversions ->
+        keyword "Print Canonical Structures"
+      | PrintTables ->
+        keyword "Print Tables"
+      | PrintHintGoal ->
+        keyword "Print Hint"
+      | PrintHint qid ->
+        keyword "Print Hint" ++ spc () ++ pr_smart_global qid
+      | PrintHintDb ->
+        keyword "Print Hint *"
+      | PrintHintDbName s ->
+        keyword "Print HintDb" ++ spc () ++ str s
+      | PrintRewriteHintDbName s ->
+        keyword "Print Rewrite HintDb" ++ spc() ++ str s
+      | PrintUniverses (b, fopt) ->
+        let cmd =
+          if b then "Print Sorted Universes"
+          else "Print Universes"
+        in
+        keyword cmd ++ pr_opt str fopt
+      | PrintName qid ->
+        keyword "Print" ++ spc()  ++ pr_smart_global qid
+      | PrintModuleType qid ->
+        keyword "Print Module Type" ++ spc() ++ pr_reference qid
+      | PrintModule qid ->
+        keyword "Print Module" ++ spc() ++ pr_reference qid
+      | PrintInspect n ->
+        keyword "Inspect" ++ spc() ++ int n
+      | PrintScopes ->
+        keyword "Print Scopes"
+      | PrintScope s ->
+        keyword "Print Scope" ++ spc() ++ str s
+      | PrintVisibility s ->
+        keyword "Print Visibility" ++ pr_opt str s
+      | PrintAbout (qid,gopt) ->
+         pr_opt (fun g -> int g ++ str ":"++ spc()) gopt
+	 ++ keyword "About" ++ spc()  ++ pr_smart_global qid
+      | PrintImplicit qid ->
+        keyword "Print Implicit" ++ spc()  ++ pr_smart_global qid
+      (* 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"
+          | true, false -> "Print Opaque Dependencies"
+          | false, true -> "Print Transparent Dependencies"
+          | false, false -> "Print Assumptions"
+        in
+        keyword cmd ++ spc() ++ pr_smart_global qid
+      | PrintNamespace dp ->
+        keyword "Print Namespace" ++ pr_dirpath dp
+      | PrintStrategy None ->
+        keyword "Print Strategies"
+      | PrintStrategy (Some qid) ->
+        keyword "Print Strategy" ++ pr_smart_global qid
+    in
+
+    let pr_using e = str (Proof_using.to_string e) in
+
+    let rec pr_vernac v =
+      let return = Taggers.tag_vernac v in
+      match v with
+        | VernacPolymorphic (poly, v) ->
+          let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in
+          return (s ++ pr_vernac v)
+        | VernacProgram v ->
+          return (keyword "Program" ++ spc() ++ pr_vernac v)
+        | VernacLocal (local, v) ->
+          return (pr_locality local ++ spc() ++ pr_vernac v)
+
+        (* Stm *)
+        | VernacStm JoinDocument ->
+          return (keyword "Stm JoinDocument")
+        | VernacStm PrintDag ->
+          return (keyword "Stm PrintDag")
+        | VernacStm Finish ->
+          return (keyword "Stm Finish")
+        | VernacStm Wait ->
+          return (keyword "Stm Wait")
+        | VernacStm (Observe id) ->
+          return (keyword "Stm Observe " ++ str(Stateid.to_string id))
+        | VernacStm (Command v) ->
+          return (keyword "Stm Command " ++ pr_vernac v)
+        | VernacStm (PGLast v) ->
+          return (keyword "Stm PGLast " ++ pr_vernac v)
+
+        (* Proof management *)
+        | VernacAbortAll ->
+          return (keyword "Abort All")
+        | VernacRestart ->
+          return (keyword "Restart")
+        | VernacUnfocus ->
+          return (keyword "Unfocus")
+        | VernacUnfocused ->
+          return (keyword "Unfocused")
+        | VernacGoal c ->
+          return (keyword "Goal" ++ pr_lconstrarg c)
+        | VernacAbort id ->
+          return (keyword "Abort" ++ pr_opt pr_lident id)
+        | VernacUndo i ->
+          return (
+            if Int.equal i 1 then keyword "Undo" else keyword "Undo" ++ pr_intarg i
+          )
+        | VernacUndoTo i ->
+          return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i)
+        | VernacBacktrack (i,j,k) ->
+          return (keyword "Backtrack" ++  spc() ++ prlist_with_sep sep int [i;j;k])
+        | VernacFocus i ->
+          return (keyword "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 -> keyword "Show" ++ pr_goal_reference n
+            | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n
+            | ShowProof -> keyword "Show Proof"
+            | ShowNode -> keyword "Show Node"
+            | ShowScript -> keyword "Show Script"
+            | ShowExistentials -> keyword "Show Existentials"
+            | ShowUniverses -> keyword "Show Universes"
+            | ShowTree -> keyword "Show Tree"
+            | ShowProofNames -> keyword "Show Conjectures"
+            | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
+            | ShowMatch id -> keyword "Show Match " ++ pr_lident id
+            | ShowThesis -> keyword "Show Thesis"
+          in
+          return (pr_showable s)
+        | VernacCheckGuard ->
+          return (keyword "Guarded")
+
+      (* Resetting *)
+        | VernacResetName id ->
+          return (keyword "Reset" ++ spc() ++ pr_lident id)
+        | VernacResetInitial ->
+          return (keyword "Reset Initial")
+        | VernacBack i ->
+          return (
+            if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i
+          )
+        | VernacBackTo i ->
+          return (keyword "BackTo" ++ pr_intarg i)
+
+      (* State management *)
+        | VernacWriteState s ->
+          return (keyword "Write State" ++ spc () ++ qs s)
+        | VernacRestoreState s ->
+          return  (keyword "Restore State" ++ spc() ++ qs s)
+
+      (* Control *)
+        | VernacLoad (f,s) ->
+          return (
+            keyword "Load"
+            ++ if f then
+                (spc() ++ keyword "Verbose" ++ spc())
+              else
+                spc() ++ qs s
+          )
+        | VernacTime v ->
+          return (keyword "Time" ++ spc() ++ pr_vernac_list v)
+        | VernacTimeout(n,v) ->
+          return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v)
+        | VernacFail v ->
+          return (keyword "Fail" ++ spc() ++ pr_vernac v)
+        | VernacError _ ->
+          return (keyword "No-parsing-rule for VernacError")
+
+      (* Syntax *)
+        | VernacTacticNotation (n,r,e) ->
+          return (pr_grammar_tactic_rule n ("",r,e))
+        | VernacOpenCloseScope (_,(opening,sc)) ->
+          return (
+            keyword (if opening then "Open " else "Close ") ++
+              keyword "Scope" ++ spc() ++ str sc
+          )
+        | VernacDelimiters (sc,key) ->
+          return (
+            keyword "Delimit Scope" ++ spc () ++ str sc ++
+              spc() ++ keyword "with" ++ spc () ++ str key
+          )
+        | VernacBindScope (sc,cll) ->
+          return (
+            keyword "Bind Scope" ++ spc () ++ str sc ++
+              spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_smart_global cll
+          )
+        | VernacArgumentsScope (q,scl) ->
+          let pr_opt_scope = function
+            | None -> str"_"
+            | Some sc -> str sc
+          in
+          return (
+            keyword "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 (keyword "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 (keyword "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 (
+            keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++
+              pr_syntax_modifiers l
+          )
+        | VernacNotationAddFormat(s,k,v) ->
+          return (
+            keyword "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
+            keyword (Kindops.string_of_definition_kind (l,false,dk))
+          in
+          let pr_reduce = function
+            | None -> mt()
+            | Some r ->
+              keyword "Eval" ++ spc() ++
+                pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++
+                keyword " 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 () ++ keyword "with")) (List.tl l))
+          )
+
+        | VernacEndProof Admitted ->
+          return (keyword "Admitted")
+
+        | VernacEndProof (Proved (opac,o)) -> return (
+          match o with
+            | None -> if opac then keyword "Qed" else keyword "Defined"
+            | Some (id,th) -> (match th with
+                | None -> (if opac then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
+                | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)
+        )
+        | VernacExactProof c ->
+          return (hov 2 (keyword "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
+          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 ++ keyword "Fixpoint" ++ spc () ++
+                     prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs)
+          )
+
+        | VernacCoFixpoint (local, corecs) ->
+          let local = match local with
+            | Some Discharge -> keyword "Let" ++ spc ()
+            | Some Local -> keyword "Local" ++ spc ()
+            | None | Some Global -> str ""
+          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 (local ++ keyword "CoFixpoint" ++ spc() ++
+                     prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs)
+          )
+        | VernacScheme l ->
+          return (
+            hov 2 (keyword "Scheme" ++ spc() ++
+                     prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onescheme l)
+          )
+        | VernacCombinedScheme (id, l) ->
+          return (
+            hov 2 (keyword "Combined Scheme" ++ spc() ++
+                     pr_lident id ++ spc() ++ keyword "from" ++ spc() ++
+                     prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
+          )
+        | VernacUniverse v ->
+          return (
+            hov 2 (keyword "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 (keyword "Constraint" ++ spc () ++
+                     prlist_with_sep (fun _ -> str",") pr_uconstraint v)
+          )
+
+        (* Gallina extensions *)
+        | VernacBeginSection id ->
+          return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id))
+        | VernacEndSegment id ->
+          return (hov 2 (keyword "End" ++ spc() ++ pr_lident id))
+        | VernacNameSectionHypSet (id,set) ->
+          return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++
+          str ":="++spc()++pr_using set))
+        | VernacRequire (exp, l) ->
+          return (
+            hov 2
+              (keyword "Require" ++ spc() ++ pr_require_token exp ++
+                 prlist_with_sep sep pr_module l)
+          )
+        | VernacImport (f,l) ->
+          return (
+            (if f then keyword "Export" else keyword "Import") ++ spc() ++
+              prlist_with_sep sep pr_import_module l
+          )
+        | VernacCanonical q ->
+          return (
+            keyword "Canonical Structure" ++ spc() ++ pr_smart_global q
+          )
+        | VernacCoercion (_,id,c1,c2) ->
+          return (
+            hov 1 (
+              keyword "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 (
+              keyword "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 keyword "Declare" ++ spc () else mt ()) ++
+                keyword "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 (
+              keyword "Context" ++ spc () ++ pr_and_type_binders_arg l)
+          )
+
+        | VernacDeclareInstances (ids, pri) ->
+          return (
+            hov 1 (keyword "Existing" ++ spc () ++
+                     keyword(String.plural (List.length ids) "Instance") ++
+                     spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri)
+          )
+
+        | VernacDeclareClass id ->
+          return (
+            hov 1 (keyword "Existing" ++ spc () ++ keyword "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 (keyword "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 (keyword "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 (keyword "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 (keyword "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":"
+          | SelectId id -> pr_id id ++ str":"
+          | SelectAll -> str"all" ++ str":"
+          | SelectAllParallel -> str"par"
+        in
+        let pr_info =
+          match info with
+            | None -> mt ()
+            | Some i -> str"Info"++spc()++int i++spc()
+        in
+        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) ->
+          return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
+
+        (* Auxiliary file and library management *)
+        | VernacAddLoadPath (fl,s,d) ->
+          return (
+            hov 2
+              (keyword "Add" ++
+                 (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++
+                 keyword "LoadPath" ++ spc() ++ qs s ++
+                 (match d with
+                   | None -> mt()
+                   | Some dir -> spc() ++ keyword "as" ++ spc() ++ pr_dirpath dir))
+          )
+        | VernacRemoveLoadPath s ->
+          return (keyword "Remove LoadPath" ++ qs s)
+        | VernacAddMLPath (fl,s) ->
+          return (
+            keyword "Add"
+            ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc())
+            ++ keyword "ML Path"
+            ++ qs s
+          )
+        | VernacDeclareMLModule (l) ->
+          return (
+            hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
+          )
+        | VernacChdir s ->
+          return (keyword "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
+              (keyword "Ltac" ++ spc () ++
+                 prlist_with_sep (fun () ->
+                   fnl() ++ keyword "with" ++ spc ()) pr_tac_body l)
+          )
+        | VernacCreateHintDb (dbname,b) ->
+          return (
+            hov 1 (keyword "Create HintDb" ++ spc () ++
+                     str dbname ++ (if b then str" discriminated" else mt ()))
+          )
+        | VernacRemoveHints (dbnames, ids) ->
+          return (
+            hov 1 (keyword "Remove Hints" ++ spc () ++
+                     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
+              (keyword "Notation" ++ spc () ++ 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 (keyword "Implicit Arguments" ++ spc() ++ pr_smart_global q)
+          )
+        | VernacDeclareImplicits (q,impls) ->
+          return (
+            hov 1 (keyword "Implicit Arguments" ++ spc () ++
+                     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 (
+              keyword "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 -> keyword "simpl nomatch"
+                      | `ReductionNeverUnfold -> keyword "simpl never"
+                      | `DefaultImplicits -> keyword "default implicits"
+                      | `Rename -> keyword "rename"
+                      | `Assert -> keyword "assert"
+                      | `ExtraScopes -> keyword "extra scopes"
+                      | `ClearImplicits -> keyword "clear implicits"
+                      | `ClearScopes -> keyword "clear scopes")
+                    mods)
+          )
+        | VernacReserve bl ->
+          let n = List.length (List.flatten (List.map fst bl)) in
+          return (
+            hov 2 (tag_keyword (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 (tag_keyword (
+              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 (keyword "Transparent" ++
+                     spc() ++ prlist_with_sep sep pr_smart_global l)
+          )
+        | VernacSetOpacity(Conv_oracle.Opaque,l) ->
+          return (
+            hov 1 (keyword "Opaque" ++
+                     spc() ++ prlist_with_sep sep pr_smart_global l)
+          )
+        | VernacSetOpacity _ ->
+          return (
+            Errors.anomaly (keyword "VernacSetOpacity used to set something else")
+          )
+        | VernacSetStrategy l ->
+          let pr_lev = function
+            | Conv_oracle.Opaque -> keyword "opaque"
+            | Conv_oracle.Expand -> keyword "expand"
+            | l when Conv_oracle.is_transparent l -> keyword "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 (keyword "Strategy" ++ spc() ++
+                     hv 0 (prlist_with_sep sep pr_line l))
+          )
+        | VernacUnsetOption (na) ->
+          return (
+            hov 1 (keyword "Unset" ++ spc() ++ pr_printoption na None)
+          )
+        | VernacSetOption (na,v) ->
+          return (
+            hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v)
+          )
+        | VernacAddOption (na,l) ->
+          return (
+            hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l))
+          )
+        | VernacRemoveOption (na,l) ->
+          return (
+            hov 2 (keyword "Remove" ++ spc() ++ pr_printoption na (Some l))
+          )
+        | VernacMemOption (na,l) ->
+          return (
+            hov 2 (keyword "Test" ++ spc() ++ pr_printoption na (Some l))
+          )
+        | VernacPrintOption na ->
+          return (
+            hov 2 (keyword "Test" ++ spc() ++ pr_printoption na None)
+          )
+        | VernacCheckMayEval (r,io,c) ->
+          let pr_mayeval r c = match r with
+            | Some r0 ->
+              hov 2 (keyword "Eval" ++ spc() ++
+                       pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++
+                       spc() ++ keyword "in" ++ spc () ++ pr_lconstr c)
+            | None -> hov 2 (keyword "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 (keyword "Type" ++ pr_constrarg c))
+        | VernacDeclareReduction (s,r) ->
+          return (
+            keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++
+              pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r
+          )
+        | VernacPrint p ->
+          return (pr_printable p)
+        | VernacSearch (sea,g,sea_r) ->
+          return (pr_search sea g sea_r pr_constr_pattern_expr)
+        | VernacLocate loc ->
+          let pr_locate =function
+            | LocateAny qid -> pr_smart_global qid
+            | LocateTerm qid -> keyword "Term" ++ spc() ++ pr_smart_global qid
+            | LocateFile f -> keyword "File" ++ spc() ++ qs f
+            | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid
+            | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid
+            | LocateTactic qid -> keyword "Ltac" ++ spc () ++ pr_ltac_ref qid
+          in
+          return (keyword "Locate" ++ spc() ++ pr_locate loc)
+        | VernacRegister (id, RegisterInline) ->
+          return (
+            hov 2
+              (keyword "Register Inline" ++ spc() ++ pr_lident id)
+          )
+        | VernacComments l ->
+          return (
+            hov 2
+              (keyword "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 (keyword "Proof")
+        | VernacProof (None, Some e) ->
+          return (keyword "Proof " ++ spc () ++
+              keyword "using" ++ spc() ++ pr_using e)
+        | VernacProof (Some te, None) ->
+          return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te)
+        | VernacProof (Some te, Some e) ->
+          return (
+            keyword "Proof" ++ spc () ++
+              keyword "using" ++ spc() ++ pr_using e ++ spc() ++
+              keyword "with" ++ spc() ++pr_raw_tactic te
+          )
+        | VernacProofMode s ->
+          return (keyword "Proof Mode" ++ str 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 (keyword "BeginSubproof" ++ spc () ++ int i)
+        | VernacEndSubproof ->
+          return (str "}")
+
+    and pr_vernac_list l =
+      hov 2 (str"[" ++ spc() ++
+               prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l
+             ++ spc() ++ str"]")
+
+    and pr_extend s cl =
+      let pr_arg a =
+        try pr_gen a
+        with Failure _ -> str ("<error in "^fst s^">") in
+      try
+        let rl = Egramml.get_extend_vernac_rule s in
+        let start,rl,cl =
+          match rl with
+            | Egramml.GramTerminal s :: rl -> str s, rl, cl
+            | Egramml.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl
+            | [] -> anomaly (Pp.str "Empty entry") in
+        let (pp,_) =
+          List.fold_left
+            (fun (strm,args) pi ->
+              let pp,args = match pi with
+                | Egramml.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args)
+                | Egramml.GramTerminal s -> (str s, args) in
+              (strm ++ spc() ++ pp), args)
+            (start,cl) rl in
+        hov 1 pp
+      with Not_found ->
+        hov 1 (str ("TODO("^fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
+
+    in pr_vernac
+
+  let pr_vernac_body v = make_pr_vernac pr_constr_expr pr_lconstr_expr v
+
+  let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end v
+
+  let pr_vernac x =
+    try pr_vernac x
+    with e -> Errors.print e
+
+end
+
+include Make (Ppconstr) (Pptactic) (struct
+  let do_not_tag _ x = x
+  let tag_keyword = do_not_tag ()
+  let tag_vernac  = do_not_tag
+end)
+
+module Richpp = struct
+
+  include Make
+    (Ppconstr.Richpp)
+    (Pptactic.Richpp)
+    (struct
+      open Ppannotation
+      let tag_keyword s = Pp.tag (Pp.Tag.inj AKeyword tag) s
+      let tag_vernac v s = Pp.tag (Pp.Tag.inj (AVernac v) tag) s
+     end)
+
+end
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
new file mode 100644
index 00000000..f38848cd
--- /dev/null
+++ b/printing/ppvernac.mli
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This module implements pretty-printers for vernac_expr syntactic
+    objects and their subcomponents. *)
+
+(** The default pretty-printers produce {!Pp.std_ppcmds} that are
+    interpreted as raw strings. *)
+include Ppvernacsig.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}. *)
+module Richpp : Ppvernacsig.Pp
diff --git a/printing/ppvernacsig.mli b/printing/ppvernacsig.mli
new file mode 100644
index 00000000..cfcd4974
--- /dev/null
+++ b/printing/ppvernacsig.mli
@@ -0,0 +1,17 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module type Pp = sig
+
+  (** Prints a vernac expression *)
+  val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds
+
+  (** Prints a vernac expression and closes it with a dot. *)
+  val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds
+
+end
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
new file mode 100644
index 00000000..223377c2
--- /dev/null
+++ b/printing/prettyp.ml
@@ -0,0 +1,852 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Changed by (and thus parts copyright ©) by Lionel Elie Mamane <lionel@mamane.lu>
+ * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
+ *)
+
+open Pp
+open Errors
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Declarations
+open Environ
+open Impargs
+open Libobject
+open Libnames
+open Globnames
+open Recordops
+open Misctypes
+open Printer
+open Printmod
+
+type object_pr = {
+  print_inductive           : mutual_inductive -> std_ppcmds;
+  print_constant_with_infos : constant -> std_ppcmds;
+  print_section_variable    : variable -> std_ppcmds;
+  print_syntactic_def       : kernel_name -> std_ppcmds;
+  print_module              : bool -> Names.module_path -> std_ppcmds;
+  print_modtype             : module_path -> std_ppcmds;
+  print_named_decl          : Id.t * constr option * types -> std_ppcmds;
+  print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
+  print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
+  print_typed_value_in_env  : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds;
+  print_eval                : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds;
+}
+
+let gallina_print_module  = print_module
+let gallina_print_modtype = print_modtype
+
+(**************)
+(** Utilities *)
+
+let print_closed_sections = ref false
+
+let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l)
+
+let with_line_skip l = if List.is_empty l then mt() else fnl() ++ fnl () ++ pr_infos_list l
+
+let blankline = mt() (* add a blank sentence in the list of infos *)
+
+let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": "
+
+let int_or_no n = if Int.equal n 0 then str "no" else int n
+
+(*******************)
+(** Basic printing *)
+
+let print_basename sp = pr_global (ConstRef sp)
+
+let print_ref reduce ref =
+  let typ = Global.type_of_global_unsafe ref in
+  let typ =
+    if reduce then
+      let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ
+      in it_mkProd_or_LetIn ccl ctx
+    else typ in
+  let univs = Global.universes_of_global ref in
+  hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ ++ 
+  	   Printer.pr_universe_ctx univs)
+
+(********************************)
+(** Printing implicit arguments *)
+
+let pr_impl_name imp = pr_id (name_of_implicit imp)
+
+let print_impargs_by_name max = function
+  | []  -> []
+  | impls ->
+     let n = List.length impls in
+     [hov 0 (str (String.plural n "Argument") ++ spc() ++
+      prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++
+      str (String.conjugate_verb_to_be n) ++ str" implicit" ++
+      (if max then strbrk " and maximally inserted" else mt()))]
+
+let print_one_impargs_list l =
+  let imps = List.filter is_status_implicit l in
+  let maximps = List.filter Impargs.maximal_insertion_of imps in
+  let nonmaximps = List.subtract Pervasives.(=) imps maximps in (* FIXME *)
+  print_impargs_by_name false nonmaximps @
+  print_impargs_by_name true maximps
+
+let print_impargs_list prefix l =
+  let l = extract_impargs_data l in
+  List.flatten (List.map (fun (cond,imps) ->
+    match cond with
+    | None ->
+	List.map (fun pp -> add_colon prefix ++ pp)
+	  (print_one_impargs_list imps)
+    | Some (n1,n2) ->
+       [v 2 (prlist_with_sep cut (fun x -> x)
+	 [(if ismt prefix then str "When" else prefix ++ str ", when") ++
+	   str " applied to " ++
+	   (if Int.equal n1 n2 then int_or_no n2 else
+	    if Int.equal n1 0 then str "less than " ++ int n2
+	    else int n1 ++ str " to " ++ int_or_no n2) ++
+	    str (String.plural n2 " argument") ++ str ":";
+          v 0 (prlist_with_sep cut (fun x -> x)
+	    (if List.exists is_status_implicit imps
+	    then print_one_impargs_list imps
+	    else [str "No implicit arguments"]))])]) l)
+
+let print_renames_list prefix l =
+  if List.is_empty l then [] else
+  [add_colon prefix ++ str "Arguments are renamed to " ++
+    hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))]
+
+let need_expansion impl ref =
+  let typ = Global.type_of_global_unsafe ref in
+  let ctx = prod_assum typ in
+  let nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) in
+  not (List.is_empty impl) && List.length impl >= nprods &&
+    let _,lastimpl = List.chop nprods impl in
+      List.exists is_status_implicit lastimpl
+
+let print_impargs ref =
+  let ref = Smartlocate.smart_global ref in
+  let impl = implicits_of_global ref in
+  let has_impl = not (List.is_empty impl) in
+  (* Need to reduce since implicits are computed with products flattened *)
+  pr_infos_list
+    ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref;
+       blankline ] @
+    (if has_impl then print_impargs_list (mt()) impl
+     else [str "No implicit arguments"]))
+
+(*********************)
+(** Printing Scopes  *)
+
+let print_argument_scopes prefix = function
+  | [Some sc] ->
+      [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"]
+  | l when not (List.for_all Option.is_empty l) ->
+     [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++
+      str "[" ++
+      pr_sequence (function Some sc -> str sc | None -> str "_") l ++
+      str "]")]
+  | _  -> []
+
+(*********************)
+(** Printing Opacity *)
+
+type opacity =
+  | FullyOpaque
+  | TransparentMaybeOpacified of Conv_oracle.level
+
+let opacity env = function
+  | VarRef v when not (Option.is_empty (pi2 (Environ.lookup_named v env))) ->
+      Some(TransparentMaybeOpacified
+        (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v)))
+  | ConstRef cst ->
+      let cb = Environ.lookup_constant cst env in
+      (match cb.const_body with
+	| Undef _ -> None
+	| OpaqueDef _ -> Some FullyOpaque
+	| Def _ -> Some
+          (TransparentMaybeOpacified
+            (Conv_oracle.get_strategy (Environ.oracle env) (ConstKey cst))))
+  | _ -> None
+
+let print_opacity ref =
+  match opacity (Global.env()) ref with
+    | None -> []
+    | Some s ->
+       [pr_global ref ++ str " is " ++
+        str (match s with
+          | FullyOpaque -> "opaque"
+          | TransparentMaybeOpacified Conv_oracle.Opaque ->
+              "basically transparent but considered opaque for reduction"
+          | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev ->
+              "transparent"
+          | TransparentMaybeOpacified (Conv_oracle.Level n) ->
+              "transparent (with expansion weight "^string_of_int n^")"
+          | TransparentMaybeOpacified Conv_oracle.Expand ->
+              "transparent (with minimal expansion weight)")]
+
+(*******************)
+(* *)
+
+let print_polymorphism ref =
+  let poly = Global.is_polymorphic ref in
+  let template_poly = Global.is_template_polymorphic ref in
+    pr_global ref ++ str " is " ++ str 
+      (if poly then "universe polymorphic"
+       else if template_poly then
+	 "template universe polymorphic"
+       else "not universe polymorphic")
+
+let print_primitive_record mipv = function
+  | Some (Some (_, ps,_)) ->
+    [pr_id mipv.(0).mind_typename ++ str" is primitive and has eta conversion."]
+  | _ -> []
+    
+let print_primitive ref =
+  match ref with 
+  | IndRef ind -> 
+    let mib,_ = Global.lookup_inductive ind in
+      print_primitive_record mib.mind_packets mib.mind_record
+  | _ -> []
+    
+let print_name_infos ref =
+  let poly = print_polymorphism ref in
+  let impls = implicits_of_global ref in
+  let scopes = Notation.find_arguments_scope ref in
+  let renames =
+    try List.hd (Arguments_renaming.arguments_names ref) with Not_found -> [] in
+  let type_info_for_implicit =
+    if need_expansion (select_impargs_size 0 impls) ref then
+      (* Need to reduce since implicits are computed with products flattened *)
+      [str "Expanded type for implicit arguments";
+       print_ref true ref; blankline]
+    else
+      [] in
+  poly :: print_primitive ref @
+  type_info_for_implicit @
+  print_renames_list (mt()) renames @
+  print_impargs_list (mt()) impls @
+  print_argument_scopes (mt()) scopes
+
+let print_id_args_data test pr id l =
+  if List.exists test l then
+    pr (str "For " ++ pr_id id) l
+  else
+    []
+
+let print_args_data_of_inductive_ids get test pr sp mipv =
+  List.flatten (Array.to_list (Array.mapi
+    (fun i mip ->
+      print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) @
+      List.flatten (Array.to_list (Array.mapi
+	(fun j idc ->
+	  print_id_args_data test pr idc (get (ConstructRef ((sp,i),j+1))))
+        mip.mind_consnames)))
+    mipv))
+
+let print_inductive_implicit_args =
+  print_args_data_of_inductive_ids
+    implicits_of_global (fun l -> not (List.is_empty (positions_of_implicits l)))
+    print_impargs_list
+
+let print_inductive_renames =
+  print_args_data_of_inductive_ids
+    (fun r ->
+      try List.hd (Arguments_renaming.arguments_names r) with Not_found -> [])
+    ((!=) Anonymous)
+    print_renames_list
+
+let print_inductive_argument_scopes =
+  print_args_data_of_inductive_ids
+    Notation.find_arguments_scope (Option.has_some) print_argument_scopes
+
+(*********************)
+(* "Locate" commands *)
+
+type logical_name =
+  | Term of global_reference
+  | Dir of global_dir_reference
+  | Syntactic of kernel_name
+  | ModuleType of module_path
+  | Tactic of Nametab.ltac_constant
+  | Undefined of qualid
+
+let locate_any_name ref =
+  let (loc,qid) = qualid_of_reference ref in
+  try Term (Nametab.locate qid)
+  with Not_found ->
+  try Syntactic (Nametab.locate_syndef qid)
+  with Not_found ->
+  try Dir (Nametab.locate_dir qid)
+  with Not_found ->
+  try ModuleType (Nametab.locate_modtype qid)
+  with Not_found -> Undefined qid
+
+let pr_located_qualid = function
+  | Term ref ->
+      let ref_str = match ref with
+	  ConstRef _ -> "Constant"
+	| IndRef _ -> "Inductive"
+	| ConstructRef _ -> "Constructor"
+	| VarRef _ -> "Variable" in
+      str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref)
+  | Syntactic kn ->
+      str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn)
+  | Dir dir ->
+      let s,dir = match dir with
+	| DirOpenModule (dir,_) -> "Open Module", dir
+	| DirOpenModtype (dir,_) -> "Open Module Type", dir
+	| DirOpenSection (dir,_) -> "Open Section", dir
+	| DirModule (dir,_) -> "Module", dir
+	| DirClosedSection dir -> "Closed Section", dir
+      in
+      str s ++ spc () ++ pr_dirpath dir
+  | ModuleType mp ->
+      str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp)
+  | Tactic kn ->
+      str "Ltac" ++ spc () ++ pr_path (Nametab.path_of_tactic kn)
+  | Undefined qid ->
+      pr_qualid qid ++ spc () ++ str "not a defined object."
+
+let canonize_ref = function
+  | ConstRef c ->
+    let kn = Constant.canonical c in
+    if KerName.equal (Constant.user c) kn then None
+    else Some (ConstRef (Constant.make1 kn))
+  | IndRef (ind,i) ->
+    let kn = MutInd.canonical ind in
+    if KerName.equal (MutInd.user ind) kn then None
+    else Some (IndRef (MutInd.make1 kn, i))
+  | ConstructRef ((ind,i),j) ->
+    let kn = MutInd.canonical ind in
+    if KerName.equal (MutInd.user ind) kn then None
+    else Some (ConstructRef ((MutInd.make1 kn, i),j))
+  | VarRef _ -> None
+
+let display_alias = function
+  | Term r ->
+    begin match canonize_ref r with
+    | None -> mt ()
+    | Some r' ->
+      let q' = Nametab.shortest_qualid_of_global Id.Set.empty r' in
+      spc () ++ str "(alias of " ++ pr_qualid q' ++ str ")"
+    end
+  | _ -> mt ()
+
+let locate_term qid =
+  let expand = function
+    | TrueGlobal ref ->
+        Term ref, Nametab.shortest_qualid_of_global Id.Set.empty ref
+    | SynDef kn ->
+        Syntactic kn, Nametab.shortest_qualid_of_syndef Id.Set.empty kn
+  in
+  List.map expand (Nametab.locate_extended_all qid)
+
+let locate_tactic qid =
+  let all = Nametab.locate_extended_all_tactic qid in
+  List.map (fun kn -> (Tactic kn, Nametab.shortest_qualid_of_tactic kn)) all
+
+let locate_module qid =
+  let all = Nametab.locate_extended_all_dir qid in
+  let map dir = match dir with
+  | DirModule (_, (mp, _)) -> Some (Dir dir, Nametab.shortest_qualid_of_module mp)
+  | DirOpenModule _ -> Some (Dir dir, qid)
+  | _ -> None
+  in
+  List.map_filter map all
+
+let locate_modtype qid =
+  let all = Nametab.locate_extended_all_modtype qid in
+  let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in
+  let modtypes = List.map map all in
+  (** Don't forget the opened module types: they are not part of the same name tab. *)
+  let all = Nametab.locate_extended_all_dir qid in
+  let map dir = match dir with
+  | DirOpenModtype _ -> Some (Dir dir, qid)
+  | _ -> None
+  in
+  modtypes @ List.map_filter map all
+
+let print_located_qualid name flags ref =
+  let (loc,qid) = qualid_of_reference ref in
+  let located = [] in
+  let located = if List.mem `LTAC flags then locate_tactic qid @ located else located in
+  let located = if List.mem `MODTYPE flags then locate_modtype qid @ located else located in
+  let located = if List.mem `MODULE flags then locate_module qid @ located else located in
+  let located = if List.mem `TERM flags then locate_term qid @ located else located in
+  match located with
+    | [] ->
+	let (dir,id) = repr_qualid qid in
+	if DirPath.is_empty dir then
+	  str ("No " ^ name ^ " of basename") ++ spc () ++ pr_id id
+	else
+	  str ("No " ^ name ^ " of suffix") ++ spc () ++ pr_qualid qid
+    | l ->
+	prlist_with_sep fnl
+	(fun (o,oqid) ->
+	  hov 2 (pr_located_qualid o ++
+	  (if not (qualid_eq oqid qid) then
+	    spc() ++ str "(shorter name to refer to it in current context is "
+            ++ pr_qualid oqid ++ str")"
+	   else mt ()) ++
+          display_alias o)) l
+
+let print_located_term ref = print_located_qualid "term" [`TERM] ref
+let print_located_tactic ref = print_located_qualid "tactic" [`LTAC] ref
+let print_located_module ref = print_located_qualid "module" [`MODULE; `MODTYPE] ref
+let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MODULE; `MODTYPE] ref
+
+(******************************************)
+(**** Printing declarations and judgments *)
+(****  Gallina layer                  *****)
+
+let gallina_print_typed_value_in_env env sigma (trm,typ) =
+  (pr_lconstr_env env sigma trm ++ fnl () ++
+     str "     : " ++ pr_ltype_env env sigma typ)
+
+(* To be improved; the type should be used to provide the types in the
+   abstractions. This should be done recursively inside pr_lconstr, so that
+   the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
+   synthesizes the type nat of the abstraction on u *)
+
+let print_named_def name body typ =
+  let pbody = pr_lconstr body in
+  let ptyp = pr_ltype typ in
+  let pbody = if isCast body then surround pbody else pbody in
+  (str "*** [" ++ str name ++ str " " ++
+     hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
+	      str ":" ++ brk (1,2) ++ ptyp) ++
+	   str "]")
+
+let print_named_assum name typ =
+  str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]"
+
+let gallina_print_named_decl (id,c,typ) =
+  let s = Id.to_string id in
+  match c with
+    | Some body -> print_named_def s body typ
+    | None -> print_named_assum s typ
+
+let assumptions_for_print lna =
+  List.fold_right (fun na env -> add_name na env) lna empty_names_context
+
+(*********************)
+(* *)
+
+let gallina_print_inductive sp =
+  let env = Global.env() in
+  let mib = Environ.lookup_mind sp env in
+  let mipv = mib.mind_packets in
+  pr_mutual_inductive_body env sp mib ++
+  with_line_skip
+    (print_primitive_record mipv mib.mind_record @
+     print_inductive_renames sp mipv @
+     print_inductive_implicit_args sp mipv @
+     print_inductive_argument_scopes sp mipv)
+
+let print_named_decl id =
+  gallina_print_named_decl (Global.lookup_named id) ++ fnl ()
+
+let gallina_print_section_variable id =
+  print_named_decl id ++
+  with_line_skip (print_name_infos (VarRef id))
+
+let print_body = function
+  | Some c  -> pr_lconstr c
+  | None -> (str"<no body>")
+
+let print_typed_body (val_0,typ) =
+  (print_body val_0 ++ fnl () ++ str "     : " ++ pr_ltype typ)
+
+let ungeneralized_type_of_constant_type t = 
+  Typeops.type_of_constant_type (Global.env ()) t
+
+let print_constant with_values sep sp =
+  let cb = Global.lookup_constant sp in
+  let val_0 = Global.body_of_constant_body cb in
+  let typ = Declareops.type_of_constant cb in
+  let typ = ungeneralized_type_of_constant_type typ in
+  let univs = Univ.instantiate_univ_context 
+    (Global.universes_of_constant_body cb)
+  in
+  hov 0 (pr_polymorphic cb.const_polymorphic ++
+    match val_0 with
+    | None ->
+	str"*** [ " ++
+	print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++
+	str" ]" ++
+	Printer.pr_universe_ctx univs
+    | _ ->
+	print_basename sp ++ str sep ++ cut () ++
+	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++
+        Printer.pr_universe_ctx univs)
+
+let gallina_print_constant_with_infos sp =
+  print_constant true " = " sp ++
+  with_line_skip (print_name_infos (ConstRef sp))
+
+let gallina_print_syntactic_def kn =
+  let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn
+  and (vars,a) = Syntax_def.search_syntactic_definition kn in
+  let c = Notation_ops.glob_constr_of_notation_constr Loc.ghost a in
+  hov 2
+    (hov 4
+       (str "Notation " ++ pr_qualid qid ++
+        prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++
+        spc () ++ str ":=") ++
+     spc () ++
+     Constrextern.without_specific_symbols
+       [Notation.SynDefRule kn] pr_glob_constr c)
+
+let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
+  let sep = if with_values then " = " else " : "
+  and tag = object_tag lobj in
+    match (oname,tag) with
+      | (_,"VARIABLE") ->
+	  (* Outside sections, VARIABLES still exist but only with universes
+             constraints *)
+	  (try Some(print_named_decl (basename sp)) with Not_found -> None)
+      | (_,"CONSTANT") ->
+	  Some (print_constant with_values sep (constant_of_kn kn))
+      | (_,"INDUCTIVE") ->
+	  Some (gallina_print_inductive (mind_of_kn kn))
+      | (_,"MODULE") ->
+	  let (mp,_,l) = repr_kn kn in
+	    Some (print_module with_values (MPdot (mp,l)))
+      | (_,"MODULE TYPE") ->
+	  let (mp,_,l) = repr_kn kn in
+	  Some (print_modtype (MPdot (mp,l)))
+      | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
+	    "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
+      (* To deal with forgotten cases... *)
+      | (_,s) -> None
+
+let gallina_print_library_entry with_values ent =
+  let pr_name (sp,_) = pr_id (basename sp) in
+  match ent with
+    | (oname,Lib.Leaf lobj) ->
+	gallina_print_leaf_entry with_values (oname,lobj)
+    | (oname,Lib.OpenedSection (dir,_)) ->
+        Some (str " >>>>>>> Section " ++ pr_name oname)
+    | (oname,Lib.ClosedSection _) ->
+        Some (str " >>>>>>> Closed Section " ++ pr_name oname)
+    | (_,Lib.CompilingLibrary (dir,_)) ->
+	Some (str " >>>>>>> Library " ++ pr_dirpath dir)
+    | (oname,Lib.OpenedModule _) ->
+	Some (str " >>>>>>> Module " ++ pr_name oname)
+    | (oname,Lib.ClosedModule _) ->
+        Some (str " >>>>>>> Closed Module " ++ pr_name oname)
+    | (_,Lib.FrozenState _) ->
+	None
+
+let gallina_print_context with_values =
+  let rec prec n = function
+    | h::rest when Option.is_empty n || Option.get n > 0 ->
+	(match gallina_print_library_entry with_values h with
+	  | None -> prec n rest
+	  | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ())
+    | _ -> mt ()
+  in
+  prec
+
+let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} =
+  let ntrm = red_fun env sigma trm in
+  (str "     = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ))
+
+(******************************************)
+(**** Printing abstraction layer          *)
+
+let default_object_pr = {
+  print_inductive           = gallina_print_inductive;
+  print_constant_with_infos = gallina_print_constant_with_infos;
+  print_section_variable    = gallina_print_section_variable;
+  print_syntactic_def       = gallina_print_syntactic_def;
+  print_module              = gallina_print_module;
+  print_modtype             = gallina_print_modtype;
+  print_named_decl          = gallina_print_named_decl;
+  print_library_entry       = gallina_print_library_entry;
+  print_context             = gallina_print_context;
+  print_typed_value_in_env  = gallina_print_typed_value_in_env;
+  print_eval                = gallina_print_eval;
+}
+
+let object_pr = ref default_object_pr
+let set_object_pr = (:=) object_pr
+
+let print_inductive x = !object_pr.print_inductive x
+let print_constant_with_infos c = !object_pr.print_constant_with_infos c
+let print_section_variable c = !object_pr.print_section_variable c
+let print_syntactic_def x = !object_pr.print_syntactic_def x
+let print_module x  = !object_pr.print_module  x
+let print_modtype x = !object_pr.print_modtype x
+let print_named_decl x = !object_pr.print_named_decl x
+let print_library_entry x = !object_pr.print_library_entry x
+let print_context x = !object_pr.print_context x
+let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x
+let print_eval x = !object_pr.print_eval x
+
+(******************************************)
+(**** Printing declarations and judgments *)
+(****  Abstract layer                 *****)
+
+let print_typed_value x = print_typed_value_in_env (Global.env ()) Evd.empty x
+
+let print_judgment env sigma {uj_val=trm;uj_type=typ} =
+  print_typed_value_in_env env sigma (trm, typ)
+
+let print_safe_judgment env sigma j =
+  let trm = Safe_typing.j_val j in
+  let typ = Safe_typing.j_type j in
+  print_typed_value_in_env env sigma (trm, typ)
+
+(*********************)
+(* *)
+
+let print_full_context () = print_context true None (Lib.contents ())
+let print_full_context_typ () = print_context false None (Lib.contents ())
+
+let print_full_pure_context () =
+  let rec prec = function
+  | ((_,kn),Lib.Leaf lobj)::rest ->
+      let pp = match object_tag lobj with
+      | "CONSTANT" ->
+	  let con = Global.constant_of_delta_kn kn in
+	  let cb = Global.lookup_constant con in
+	  let typ = ungeneralized_type_of_constant_type cb.const_type in
+	  hov 0 (
+	    match cb.const_body with
+	      | Undef _ ->
+		str "Parameter " ++
+		print_basename con ++ str " : " ++ cut () ++ pr_ltype typ
+	      | OpaqueDef lc ->
+		str "Theorem " ++ print_basename con ++ cut () ++
+		str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++
+		str "Proof " ++ pr_lconstr (Opaqueproof.force_proof (Global.opaque_tables ()) lc)
+	      | Def c ->
+		str "Definition " ++ print_basename con ++ cut () ++
+		str "  : " ++ pr_ltype typ ++ cut () ++ str " := " ++
+		pr_lconstr (Mod_subst.force_constr c))
+          ++ str "." ++ fnl () ++ fnl ()
+      | "INDUCTIVE" ->
+	  let mind = Global.mind_of_delta_kn kn in
+	  let mib = Global.lookup_mind mind in
+	  pr_mutual_inductive_body (Global.env()) mind mib ++
+	    str "." ++ fnl () ++ fnl ()
+      | "MODULE" ->
+	  (* TODO: make it reparsable *)
+	  let (mp,_,l) = repr_kn kn in
+	  print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
+      | "MODULE TYPE" ->
+	  (* TODO: make it reparsable *)
+	  (* TODO: make it reparsable *)
+	  let (mp,_,l) = repr_kn kn in
+	  print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
+      | _ -> mt () in
+      prec rest ++ pp
+  | _::rest -> prec rest
+  | _ -> mt () in
+  prec (Lib.contents ())
+
+(* For printing an inductive definition with
+   its constructors and elimination,
+   assume that the declaration of constructors and eliminations
+   follows the definition of the inductive type *)
+
+(* This is designed to print the contents of an opened section *)
+let read_sec_context r =
+  let loc,qid = qualid_of_reference r in
+  let dir =
+    try Nametab.locate_section qid
+    with Not_found ->
+      user_err_loc (loc,"read_sec_context", str "Unknown section.") in
+  let rec get_cxt in_cxt = function
+    | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest ->
+        if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
+    | (_,Lib.ClosedSection _)::rest ->
+        error "Cannot print the contents of a closed section."
+	(* LEM: Actually, we could if we wanted to. *)
+    | [] -> []
+    | hd::rest -> get_cxt (hd::in_cxt) rest
+  in
+  let cxt = Lib.contents () in
+  List.rev (get_cxt [] cxt)
+
+let print_sec_context sec =
+  print_context true None (read_sec_context sec)
+
+let print_sec_context_typ sec =
+  print_context false None (read_sec_context sec)
+
+let print_any_name = function
+  | Term (ConstRef sp) -> print_constant_with_infos sp
+  | Term (IndRef (sp,_)) -> print_inductive sp
+  | Term (ConstructRef ((sp,_),_)) -> print_inductive sp
+  | Term (VarRef sp) -> print_section_variable sp
+  | Syntactic kn -> print_syntactic_def kn
+  | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
+  | Dir _ -> mt ()
+  | ModuleType mp -> print_modtype mp
+  | Tactic kn -> mt () (** TODO *)
+  | Undefined qid ->
+  try  (* Var locale de but, pas var de section... donc pas d'implicits *)
+    let dir,str = repr_qualid qid in
+    if not (DirPath.is_empty dir) then raise Not_found;
+    let (_,c,typ) = Global.lookup_named str in
+    (print_named_decl (str,c,typ))
+  with Not_found ->
+    errorlabstrm
+      "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
+
+let print_name = function
+  | ByNotation (loc,ntn,sc) ->
+      print_any_name
+        (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
+               ntn sc))
+  | AN ref ->
+      print_any_name (locate_any_name ref)
+
+let print_opaque_name qid =
+  let env = Global.env () in
+  match Nametab.global qid with
+    | ConstRef cst ->
+	let cb = Global.lookup_constant cst in
+        if Declareops.constant_has_body cb then
+	  print_constant_with_infos cst
+        else
+	  error "Not a defined constant."
+    | IndRef (sp,_) ->
+        print_inductive sp
+    | ConstructRef cstr as gr ->
+	let ty = Universes.unsafe_type_of_global gr in
+	print_typed_value (mkConstruct cstr, ty)
+    | VarRef id ->
+        let (_,c,ty) = lookup_named id env in
+	print_named_decl (id,c,ty)
+
+let print_about_any loc k =
+  match k with
+  | Term ref ->
+    let rb = Reductionops.ReductionBehaviour.print ref in
+    Dumpglob.add_glob loc ref;
+      pr_infos_list
+       (print_ref false ref :: blankline ::
+	print_name_infos ref @
+	(if Pp.ismt rb then [] else [rb]) @
+	print_opacity ref @
+	[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
+  | Syntactic kn ->
+    let () = match Syntax_def.search_syntactic_definition kn with
+    | [],Notation_term.NRef ref -> Dumpglob.add_glob loc ref
+    | _ -> () in
+      v 0 (
+      print_syntactic_def kn ++ fnl () ++
+      hov 0 (str "Expands to: " ++ pr_located_qualid k))
+  | Dir _ | ModuleType _ | Tactic _ | Undefined _ ->
+      hov 0 (pr_located_qualid k)
+
+let print_about = function
+  | ByNotation (loc,ntn,sc) ->
+      print_about_any loc
+        (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
+               ntn sc))
+  | AN ref ->
+      print_about_any (loc_of_reference ref) (locate_any_name ref)
+
+(* for debug *)
+let inspect depth =
+  print_context false (Some depth) (Lib.contents ())
+
+
+(*************************************************************************)
+(* Pretty-printing functions coming from classops.ml                     *)
+
+open Classops
+
+let print_coercion_value v = pr_lconstr (get_coercion_value v)
+
+let print_class i =
+  let cl,_ = class_info_from_index i in
+  pr_class cl
+
+let print_path ((i,j),p) =
+  hov 2 (
+    str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++
+    str"] : ") ++
+  print_class i ++ str" >-> " ++ print_class j
+
+let _ = Classops.install_path_printer print_path
+
+let print_graph () =
+  prlist_with_sep fnl print_path (inheritance_graph())
+
+let print_classes () =
+  pr_sequence pr_class (classes())
+
+let print_coercions () =
+  pr_sequence print_coercion_value (coercions())
+
+let index_of_class cl =
+  try
+    fst (class_info cl)
+  with Not_found ->
+    errorlabstrm "index_of_class"
+      (pr_class cl ++ spc() ++ str "not a defined class.")
+
+let print_path_between cls clt =
+  let i = index_of_class cls in
+  let j = index_of_class clt in
+  let p =
+    try
+      lookup_path_between_class (i,j)
+    with Not_found ->
+      errorlabstrm "index_cl_of_id"
+        (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
+	 ++ str ".")
+  in
+  print_path ((i,j),p)
+
+let print_canonical_projections () =
+  prlist_with_sep fnl
+    (fun ((r1,r2),o) -> pr_cs_pattern r2 ++
+    str " <- " ++
+    pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )")
+    (canonical_projections ())
+
+(*************************************************************************)
+
+(*************************************************************************)
+(* Pretty-printing functions for type classes                     *)
+
+open Typeclasses
+
+let pr_typeclass env t =
+  print_ref false t.cl_impl
+
+let print_typeclasses () =
+  let env = Global.env () in
+    prlist_with_sep fnl (pr_typeclass env) (typeclasses ())
+
+let pr_instance env i =
+  (*   gallina_print_constant_with_infos i.is_impl *)
+  (* lighter *)
+  print_ref false (instance_impl i) ++
+  begin match instance_priority i with
+  | None -> mt ()
+  | Some i -> spc () ++ str "|" ++ spc () ++ int i
+  end
+
+let print_all_instances () =
+  let env = Global.env () in
+  let inst = all_instances () in
+    prlist_with_sep fnl (pr_instance env) inst
+
+let print_instances r =
+  let env = Global.env () in
+  let inst = instances r in
+    prlist_with_sep fnl (pr_instance env) inst
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
new file mode 100644
index 00000000..6216d4d5
--- /dev/null
+++ b/printing/prettyp.mli
@@ -0,0 +1,77 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+open Term
+open Environ
+open Reductionops
+open Libnames
+open Globnames
+open Misctypes
+
+(** A Pretty-Printer for the Calculus of Inductive Constructions. *)
+
+val assumptions_for_print : Name.t list -> Termops.names_context
+
+val print_closed_sections : bool ref
+val print_context : bool -> int option -> Lib.library_segment -> std_ppcmds
+val print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option
+val print_full_context : unit -> std_ppcmds
+val print_full_context_typ : unit -> std_ppcmds
+val print_full_pure_context : unit -> std_ppcmds
+val print_sec_context : reference -> std_ppcmds
+val print_sec_context_typ : reference -> std_ppcmds
+val print_judgment : env -> Evd.evar_map -> unsafe_judgment -> std_ppcmds
+val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> std_ppcmds
+val print_eval :
+  reduction_function -> env -> Evd.evar_map ->
+    Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds
+
+val print_name : reference or_by_notation -> std_ppcmds
+val print_opaque_name : reference -> std_ppcmds
+val print_about : reference or_by_notation -> std_ppcmds
+val print_impargs : reference or_by_notation -> std_ppcmds
+
+(** Pretty-printing functions for classes and coercions *)
+val print_graph : unit -> std_ppcmds
+val print_classes : unit -> std_ppcmds
+val print_coercions : unit -> std_ppcmds
+val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds
+val print_canonical_projections : unit -> std_ppcmds
+
+(** Pretty-printing functions for type classes and instances *)
+val print_typeclasses : unit -> std_ppcmds
+val print_instances : global_reference -> std_ppcmds
+val print_all_instances : unit -> std_ppcmds
+
+val inspect : int -> std_ppcmds
+
+(** Locate *)
+
+val print_located_qualid : reference -> std_ppcmds
+val print_located_term : reference -> std_ppcmds
+val print_located_tactic : reference -> std_ppcmds
+val print_located_module : reference -> std_ppcmds
+
+type object_pr = {
+  print_inductive           : mutual_inductive -> std_ppcmds;
+  print_constant_with_infos : constant -> std_ppcmds;
+  print_section_variable    : variable -> std_ppcmds;
+  print_syntactic_def       : kernel_name -> std_ppcmds;
+  print_module              : bool -> Names.module_path -> std_ppcmds;
+  print_modtype             : module_path -> std_ppcmds;
+  print_named_decl          : Id.t * constr option * types -> std_ppcmds;
+  print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
+  print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
+  print_typed_value_in_env  : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds;
+  print_eval                : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds
+}
+
+val set_object_pr : object_pr -> unit
+val default_object_pr : object_pr
diff --git a/printing/printer.ml b/printing/printer.ml
new file mode 100644
index 00000000..3403fb9c
--- /dev/null
+++ b/printing/printer.ml
@@ -0,0 +1,760 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+open Term
+open Vars
+open Environ
+open Globnames
+open Nametab
+open Evd
+open Proof_type
+open Refiner
+open Pfedit
+open Constrextern
+open Ppconstr
+open Declarations
+
+let emacs_str s =
+  if !Flags.print_emacs then s else ""
+let delayed_emacs_cmd s =
+  if !Flags.print_emacs then s () else str ""
+
+let get_current_context () =
+  try Pfedit.get_current_goal_context ()
+  with e when Logic.catchable_exception e ->
+    (Evd.empty, Global.env())
+
+(**********************************************************************)
+(** Terms                                                             *)
+
+(* [goal_concl_style] means that all names of goal/section variables
+   and all names of rel variables (if any) in the given env and all short
+   names of global definitions of the current module must be avoided while
+   printing bound variables.
+   Otherwise, short names of global definitions are printed qualified
+   and only names of goal/section variables and rel names that do
+   _not_ occur in the scope of the binder to be printed are avoided. *)
+
+let pr_constr_core goal_concl_style env sigma t =
+  pr_constr_expr (extern_constr goal_concl_style env sigma t)
+let pr_lconstr_core goal_concl_style env sigma t =
+  pr_lconstr_expr (extern_constr goal_concl_style env sigma t)
+
+let pr_lconstr_env env = pr_lconstr_core false env
+let pr_constr_env env = pr_constr_core false env
+let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env
+
+let pr_lconstr_goal_style_env env = pr_lconstr_core true env
+let pr_constr_goal_style_env env = pr_constr_core true env
+
+let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c
+let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c
+
+  (* NB do not remove the eta-redexes! Global.env() has side-effects... *)
+let pr_lconstr t =
+  let (sigma, env) = get_current_context () in
+  pr_lconstr_env env sigma t
+let pr_constr t =
+  let (sigma, env) = get_current_context () in
+  pr_constr_env env sigma t
+
+let pr_open_lconstr (_,c) = pr_lconstr c
+let pr_open_constr (_,c) = pr_constr c
+
+let pr_constr_under_binders_env_gen pr env sigma (ids,c) =
+  (* Warning: clashes can occur with variables of same name in env but *)
+  (* we also need to preserve the actual names of the patterns *)
+  (* So what to do? *)
+  let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in
+  pr (Termops.push_rels_assum assums env) sigma c
+
+let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env
+let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env
+
+let pr_constr_under_binders c =
+  let (sigma, env) = get_current_context () in
+  pr_constr_under_binders_env env sigma c
+let pr_lconstr_under_binders c =
+  let (sigma, env) = get_current_context () in
+  pr_lconstr_under_binders_env env sigma c
+
+let pr_type_core goal_concl_style env sigma t =
+  pr_constr_expr (extern_type goal_concl_style env sigma t)
+let pr_ltype_core goal_concl_style env sigma t =
+  pr_lconstr_expr (extern_type goal_concl_style env sigma t)
+
+let pr_goal_concl_style_env env = pr_ltype_core true env
+let pr_ltype_env env = pr_ltype_core false env
+let pr_type_env env = pr_type_core false env
+
+let pr_ltype t =
+    let (sigma, env) = get_current_context () in
+    pr_ltype_env env sigma t
+let pr_type t =
+    let (sigma, env) = get_current_context () in
+    pr_type_env env sigma t
+
+let pr_ljudge_env env sigma j =
+  (pr_lconstr_env env sigma j.uj_val, pr_lconstr_env env sigma j.uj_type)
+
+let pr_ljudge j =
+  let (sigma, env) = get_current_context () in
+  pr_ljudge_env env sigma j
+
+let pr_lglob_constr_env env c =
+  pr_lconstr_expr (extern_glob_constr (Termops.vars_of_env env) c)
+let pr_glob_constr_env env c =
+  pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c)
+
+let pr_lglob_constr c =
+  let (sigma, env) = get_current_context () in
+  pr_lglob_constr_env env c
+let pr_glob_constr c =
+  let (sigma, env) = get_current_context () in
+  pr_glob_constr_env env c
+
+let pr_closed_glob_env env sigma c =
+  pr_constr_expr (extern_closed_glob false env sigma c)
+let pr_closed_glob c =
+  let (sigma, env) = get_current_context () in
+  pr_closed_glob_env env sigma c
+
+let pr_lconstr_pattern_env env sigma c =
+  pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c)
+let pr_constr_pattern_env env sigma c =
+  pr_constr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c)
+
+let pr_cases_pattern t =
+  pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t)
+
+let pr_lconstr_pattern t =
+  let (sigma, env) = get_current_context () in
+  pr_lconstr_pattern_env env sigma t
+let pr_constr_pattern t =
+  let (sigma, env) = get_current_context () in
+  pr_constr_pattern_env env sigma t
+
+let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
+
+let _ = Termops.set_print_constr 
+  (fun env t -> pr_lconstr_expr (extern_constr ~lax:true false env Evd.empty t))
+
+let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
+
+(** Term printers resilient to [Nametab] errors *)
+
+(** When the nametab isn't up-to-date, the term printers above
+    could raise [Not_found] during [Nametab.shortest_qualid_of_global].
+    In this case, we build here a fully-qualified name based upon
+    the kernel modpath and label of constants, and the idents in
+    the [mutual_inductive_body] for the inductives and constructors
+    (needs an environment for this). *)
+
+let id_of_global env = function
+  | ConstRef kn -> Label.to_id (Constant.label kn)
+  | IndRef (kn,0) -> Label.to_id (MutInd.label kn)
+  | IndRef (kn,i) ->
+    (Environ.lookup_mind kn env).mind_packets.(i).mind_typename
+  | ConstructRef ((kn,i),j) ->
+    (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1)
+  | VarRef v -> v
+
+let rec dirpath_of_mp = function
+  | MPfile sl -> sl
+  | MPbound uid -> DirPath.make [MBId.to_id uid]
+  | MPdot (mp,l) ->
+    Libnames.add_dirpath_suffix (dirpath_of_mp mp) (Label.to_id l)
+
+let dirpath_of_global = function
+  | ConstRef kn -> dirpath_of_mp (Constant.modpath kn)
+  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+    dirpath_of_mp (MutInd.modpath kn)
+  | VarRef _ -> DirPath.empty
+
+let qualid_of_global env r =
+  Libnames.make_qualid (dirpath_of_global r) (id_of_global env r)
+
+let safe_gen f env sigma c =
+  let orig_extern_ref = Constrextern.get_extern_reference () in
+  let extern_ref loc vars r =
+    try orig_extern_ref loc vars r
+    with e when Errors.noncritical e ->
+      Libnames.Qualid (loc, qualid_of_global env r)
+  in
+  Constrextern.set_extern_reference extern_ref;
+  try
+    let p = f env sigma c in
+    Constrextern.set_extern_reference orig_extern_ref;
+    p
+  with e when Errors.noncritical e ->
+    Constrextern.set_extern_reference orig_extern_ref;
+    str "??"
+
+let safe_pr_lconstr_env = safe_gen pr_lconstr_env
+let safe_pr_constr_env = safe_gen pr_constr_env
+let safe_pr_lconstr t =
+  let (sigma, env) = get_current_context () in
+  safe_pr_lconstr_env env sigma t
+
+let safe_pr_constr t =
+  let (sigma, env) = get_current_context () in
+  safe_pr_constr_env env sigma t
+
+let pr_universe_ctx c =
+  if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
+    fnl()++pr_in_comment (fun c -> v 0 
+      (Univ.pr_universe_context Universes.pr_with_global_universes c)) c
+  else
+    mt()
+
+(**********************************************************************)
+(* Global references *)
+
+let pr_global_env = pr_global_env
+let pr_global = pr_global_env Id.Set.empty
+
+let pr_puniverses f env (c,u) =
+  f env c ++ 
+  (if !Constrextern.print_universes then
+    str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+   else mt ())
+
+let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
+let pr_existential_key = Evd.pr_existential_key
+let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev)
+let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind)
+let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr)
+
+let pr_pconstant = pr_puniverses pr_constant
+let pr_pinductive = pr_puniverses pr_inductive
+let pr_pconstructor = pr_puniverses pr_constructor
+
+let pr_evaluable_reference ref =
+  pr_global (Tacred.global_of_evaluable_reference ref)
+
+(*let pr_glob_constr t =
+  pr_lconstr (Constrextern.extern_glob_constr Id.Set.empty t)*)
+
+(*open Pattern
+
+let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*)
+
+(**********************************************************************)
+(* Contexts and declarations                                          *)
+
+let pr_var_decl_skel pr_id env sigma (id,c,typ) =
+  let pbody = match c with
+    | None ->  (mt ())
+    | Some c ->
+	(* Force evaluation *)
+	let pb = pr_lconstr_env env sigma c in
+	let pb = if isCast c then surround pb else pb in
+	(str" := " ++ pb ++ cut () ) in
+  let pt = pr_ltype_env env sigma typ in
+  let ptyp = (str" : " ++ pt) in
+  (pr_id id ++ hov 0 (pbody ++ ptyp))
+
+let pr_var_decl env sigma (id,c,typ) =
+  pr_var_decl_skel pr_id env sigma (id,c,typ)
+
+let pr_var_list_decl env sigma (l,c,typ) =
+  hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ))
+
+let pr_rel_decl env sigma (na,c,typ) =
+  let pbody = match c with
+    | None -> mt ()
+    | Some c ->
+	(* Force evaluation *)
+	let pb = pr_lconstr_env env sigma c in
+	let pb = if isCast c then surround pb else pb in
+	(str":=" ++ spc () ++ pb ++ spc ()) in
+  let ptyp = pr_ltype_env env sigma typ in
+  match na with
+  | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+  | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+
+
+(* Prints out an "env" in a nice format.  We print out the
+ * signature,then a horizontal bar, then the debruijn environment.
+ * It's printed out from outermost to innermost, so it's readable. *)
+
+(* Prints a signature, all declarations on the same line if possible *)
+let pr_named_context_of env sigma =
+  let make_decl_list env d pps = pr_var_decl env sigma d :: pps in
+  let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in
+  hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
+
+let pr_named_context env sigma ne_context =
+  hv 0 (Context.fold_named_context
+	  (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d)
+          ne_context ~init:(mt ()))
+
+let pr_rel_context env sigma rel_context =
+  pr_binders (extern_rel_context None env sigma rel_context)
+
+let pr_rel_context_of env sigma =
+  pr_rel_context env sigma (rel_context env)
+
+(* Prints an env (variables and de Bruijn). Separator: newline *)
+let pr_context_unlimited env sigma =
+  let sign_env =
+    Context.fold_named_list_context
+      (fun d pps ->
+         let pidt =  pr_var_list_decl env sigma d in
+         (pps ++ fnl () ++ pidt))
+      (Termops.compact_named_context (named_context env)) ~init:(mt ())
+  in
+  let db_env =
+    fold_rel_context
+      (fun env d pps ->
+         let pnat = pr_rel_decl env sigma d in (pps ++ fnl () ++ pnat))
+      env ~init:(mt ())
+  in
+  (sign_env ++ db_env)
+
+let pr_ne_context_of header env sigma =
+  if List.is_empty (Environ.rel_context env) &&
+    List.is_empty (Environ.named_context env)  then (mt ())
+  else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ())
+
+let pr_context_limit n env sigma =
+  let named_context = Environ.named_context env in
+  let lgsign = List.length named_context in
+  if n >= lgsign then
+    pr_context_unlimited env sigma
+  else
+    let k = lgsign-n in
+    let _,sign_env =
+      Context.fold_named_list_context
+        (fun d (i,pps) ->
+           if i < k then
+	     (i+1, (pps ++str "."))
+	   else
+             let pidt = pr_var_list_decl env sigma d in
+	     (i+1, (pps ++ fnl () ++
+		      str (emacs_str "") ++
+		      pidt)))
+        (Termops.compact_named_context (Environ.named_context env)) ~init:(0,(mt ()))
+    in
+    let db_env =
+      fold_rel_context
+        (fun env d pps ->
+           let pnat = pr_rel_decl env sigma d in
+	   (pps ++ fnl () ++
+	      str (emacs_str "") ++
+	      pnat))
+        env ~init:(mt ())
+    in
+    (sign_env ++ db_env)
+
+let pr_context_of env sigma = match Flags.print_hyps_limit () with
+  | None -> hv 0 (pr_context_unlimited env sigma)
+  | Some n -> hv 0 (pr_context_limit n env sigma)
+
+(* display goal parts (Proof mode) *)
+
+let pr_predicate pr_elt (b, elts) =
+  let pr_elts = prlist_with_sep spc pr_elt elts in
+    if b then
+      str"all" ++
+	(if List.is_empty elts then mt () else str" except: " ++ pr_elts)
+    else
+      if List.is_empty elts then str"none" else pr_elts
+
+let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p)
+let pr_idpred p = pr_predicate Nameops.pr_id (Id.Pred.elements p)
+
+let pr_transparent_state (ids, csts) =
+  hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
+	str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
+
+(* display complete goal *)
+let default_pr_goal gs =
+  let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in
+  let env = Goal.V82.env sigma g in
+  let preamb,thesis,penv,pc =
+    mt (), mt (),
+    pr_context_of env sigma,
+    pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
+  in
+    preamb ++
+    str"  " ++ hv 0 (penv ++ fnl () ++
+		       str (emacs_str "")  ++
+		       str "============================" ++ fnl ()  ++
+		       thesis ++ str " " ++  pc)
+
+(* display a goal tag *)
+let pr_goal_tag g =
+  let s = " (ID " ^ Goal.uid g ^ ")" in
+  str (emacs_str s)
+
+let display_name = false
+
+(* display a goal name *)
+let pr_goal_name sigma g =
+  if display_name then str " " ++ Pp.surround (pr_id (Evd.evar_ident g sigma))
+  else mt ()
+
+(* display the conclusion of a goal *)
+let pr_concl n sigma g =
+  let (g,sigma) = Goal.V82.nf_evar sigma g in
+  let env = Goal.V82.env sigma g in
+  let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in
+    str (emacs_str "")  ++
+      str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++
+      str " is:" ++ cut () ++ str" "  ++ pc
+
+(* display evar type: a context and a type *)
+let pr_evgl_sign sigma evi =
+  let env = evar_env evi in
+  let ps = pr_named_context_of env sigma in
+  let _, l = match Filter.repr (evar_filter evi) with
+  | None -> [], []
+  | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi)
+  in
+  let ids = List.rev_map pi1 l in
+  let warn =
+    if List.is_empty ids then mt () else
+      (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
+  in
+  let pc = pr_lconstr_env env sigma evi.evar_concl in
+  hov 0 (str"[" ++ ps ++ spc () ++ str"|- "  ++ pc ++ str"]" ++ spc () ++ warn)
+
+(* Print an existential variable *)
+
+let pr_evar sigma (evk, evi) =
+  let pegl = pr_evgl_sign sigma evi in
+  hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl)
+
+(* Print an enumerated list of existential variables *)
+let rec pr_evars_int_hd head sigma i = function
+  | [] -> mt ()
+  | (evk,evi)::rest ->
+      (hov 0 (head i ++ pr_evar sigma (evk,evi))) ++
+      (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd head sigma (i+1) rest)
+
+let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ int i ++ str " =" ++ spc ()) sigma i (Evar.Map.bindings evs)
+
+let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs)
+
+let default_pr_subgoal n sigma =
+  let rec prrec p = function
+    | [] -> error "No such goal."
+    | g::rest ->
+	if Int.equal p 1 then
+          let pg = default_pr_goal { sigma=sigma ; it=g; } in
+          v 0 (str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g 
+	       ++ str " is:" ++ cut () ++ pg)
+	else
+	  prrec (p-1) rest
+  in
+  prrec n
+
+let pr_internal_existential_key ev = str (string_of_existential ev)
+
+let emacs_print_dependent_evars sigma seeds =
+  let evars () =
+    let evars = Evarutil.gather_dependent_evars sigma seeds in
+    let evars =
+      Evar.Map.fold begin fun e i s ->
+	let e' = pr_internal_existential_key e in
+	match i with
+	| None -> s ++ str" " ++ e' ++ str " open,"
+	| Some i ->
+	  s ++ str " " ++ e' ++ str " using " ++
+	    Evar.Set.fold begin fun d s ->
+	      pr_internal_existential_key d ++ str " " ++ s
+	    end i (str ",")
+      end evars (str "")
+    in
+    fnl () ++
+    str "(dependent evars:" ++ evars ++ str ")" ++ fnl ()
+  in
+  delayed_emacs_cmd evars
+
+(* Print open subgoals. Checks for uninstantiated existential variables *)
+(* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
+(* spiwack: [pr_first] is true when the first goal must be singled out
+   and printed in its entirety. *)
+(* courtieu: in emacs mode, even less cases where the first goal is printed
+   in its entirety *)
+let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals =
+  (** Printing functions for the extra informations. *)
+  let rec print_stack a = function
+    | [] -> Pp.int a
+    | b::l -> Pp.int a ++ str"-" ++ print_stack b l
+  in
+  let print_unfocused l =
+    match l with
+    | [] -> None
+    | a::l -> Some (str"unfocused: " ++ print_stack a l)
+  in
+  let print_shelf l =
+    match l with
+    | [] -> None
+    | _ -> Some (str"shelved: " ++ Pp.int (List.length l))
+  in
+  let rec print_comma_separated_list a l =
+    match l with
+    | [] -> a
+    | b::l -> print_comma_separated_list (a++str", "++b) l
+  in
+  let print_extra_list l =
+    match l with
+    | [] -> Pp.mt ()
+    | a::l -> Pp.spc () ++ str"(" ++ print_comma_separated_list a l ++ str")"
+  in
+  let extra = Option.List.flatten [ print_unfocused stack ; print_shelf shelf ] in
+  let print_extra = print_extra_list extra in
+  let focused_if_needed =
+    let needed = not (CList.is_empty extra) && pr_first in
+    if needed then str" focused "
+    else str" " (* non-breakable space *)
+  in
+  (** Main function *)
+  let rec pr_rec n = function
+    | [] -> (mt ())
+    | g::rest ->
+        let pc = pr_concl n sigma g in
+        let prest = pr_rec (n+1) rest in
+        (cut () ++ pc ++ prest)
+  in
+  let print_multiple_goals g l =
+    if pr_first then
+      default_pr_goal { it = g ; sigma = sigma; } ++ fnl () ++
+      pr_rec 2 l
+    else 
+      pr_rec 1 (g::l)
+  in
+  match goals with
+  | [] ->
+      begin
+	match close_cmd with
+	  Some cmd ->
+	    (str "Subproof completed, now type " ++ str cmd ++
+	       str ".")
+	| None ->
+	    let exl = Evarutil.non_instantiated sigma in
+	    if Evar.Map.is_empty exl then
+	      (str"No more subgoals."
+	       ++ emacs_print_dependent_evars sigma seeds)
+	    else
+	      let pei = pr_evars_int sigma 1 exl in
+	      (str "No more subgoals but non-instantiated existential " ++
+		 str "variables:" ++ fnl () ++ (hov 0 pei)
+	       ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++
+                 str "You can use Grab Existential Variables.")
+      end
+  | [g] when not !Flags.print_emacs ->
+      let pg = default_pr_goal { it = g ; sigma = sigma; } in
+      v 0 (
+	str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra
+        ++ pr_goal_tag g ++ pr_goal_name sigma g ++ cut () ++ pg
+	++ emacs_print_dependent_evars sigma seeds
+      )
+  | g1::rest ->
+      let goals = print_multiple_goals g1 rest in
+      v 0 (
+	int(List.length rest+1) ++ focused_if_needed ++ str"subgoals" ++
+          print_extra ++
+          str ((if display_name then (fun x -> x) else emacs_str) ", subgoal 1")
+        ++ pr_goal_tag g1
+        ++ pr_goal_name sigma g1 ++ cut ()
+	++ goals
+	++ emacs_print_dependent_evars sigma seeds
+      )
+
+(**********************************************************************)
+(* Abstraction layer                                                  *)
+
+
+type printer_pr = {
+ pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
+ pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
+ pr_goal                : goal sigma -> std_ppcmds;
+}
+
+let default_printer_pr = {
+ pr_subgoals = default_pr_subgoals;
+ pr_subgoal  = default_pr_subgoal;
+ pr_goal     = default_pr_goal;
+}
+
+let printer_pr = ref default_printer_pr
+
+let set_printer_pr = (:=) printer_pr
+
+let pr_subgoals ?pr_first x = !printer_pr.pr_subgoals ?pr_first x
+let pr_subgoal  x = !printer_pr.pr_subgoal  x
+let pr_goal     x = !printer_pr.pr_goal     x
+
+(* End abstraction layer                                              *)
+(**********************************************************************)
+
+let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
+  (* spiwack: it shouldn't be the job of the printer to look up stuff
+     in the [evar_map], I did stuff that way because it was more
+     straightforward, but seriously, [Proof.proof] should return
+     [evar_info]-s instead. *)
+  let p = proof in
+  let (goals , stack , shelf, given_up, sigma ) = Proof.proof p in
+  let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in
+  let seeds = Proof.V82.top_evars p in
+  begin match goals with
+  | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
+          begin match bgoals,shelf,given_up with
+	  | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
+          | [] , [] , _ ->
+	     msg_info (str "No more goals, however there are goals you gave up. You need to go back and solve them.");
+	     fnl ()
+            ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up
+          | [] , _ , _ ->
+	    msg_info (str "All the remaining goals are on the shelf.");
+	    fnl ()
+            ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
+	  | _ , _, _ ->
+	    msg_info (str "This subproof is complete, but there are still unfocused goals." ++
+			(match Proof_global.Bullet.suggest p
+			 with None  -> str"" | Some s -> fnl () ++ str s));
+	    fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals
+	  end
+  | _ -> pr_subgoals None sigma seeds shelf stack goals
+  end
+
+let pr_nth_open_subgoal n =
+  let pf = get_pftreestate () in
+  let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
+  pr_subgoal n sigma gls
+
+let pr_goal_by_id id =
+  let p = Proof_global.give_me_the_proof () in
+  let g = Goal.get_by_uid id in
+  let pr gs =
+    v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut ()
+	 ++ pr_goal gs)
+  in
+  try
+    Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;})
+  with Not_found -> error "Invalid goal identifier."
+
+(* Elementary tactics *)
+
+let pr_prim_rule = function
+  | Cut (b,replace,id,t) ->
+     if b then
+       (* TODO: express "replace" *)
+       (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")")
+     else
+       let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in
+       (str"cut " ++ pr_constr t ++
+        str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
+
+  | FixRule (f,n,[],_) ->
+      (str"fix " ++ pr_id f ++ str"/" ++ int n)
+
+  | FixRule (f,n,others,j) ->
+      if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
+      let rec print_mut = function
+	| (f,n,ar)::oth ->
+           pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
+        | [] -> mt () in
+      (str"fix " ++ pr_id f ++ str"/" ++ int n ++
+         str" with " ++ print_mut others)
+
+  | Cofix (f,[],_) ->
+      (str"cofix " ++ pr_id f)
+
+  | Cofix (f,others,j) ->
+      if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
+      let rec print_mut = function
+	| (f,ar)::oth ->
+	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
+        | [] -> mt () in
+      (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
+  | Refine c ->
+      str(if Termops.occur_meta c then "refine " else "exact ") ++
+      Constrextern.with_meta_as_hole pr_constr c
+
+  | Thin ids ->
+      (str"clear "  ++ pr_sequence pr_id ids)
+
+  | Move (id1,id2) ->
+      (str"move "  ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
+
+(* Backwards compatibility *)
+
+let prterm = pr_lconstr
+
+
+(* Printer function for sets of Assumptions.assumptions.
+   It is used primarily by the Print Assumptions command. *)
+
+open Assumptions
+
+let pr_assumptionset env s =
+  if ContextObjectMap.is_empty s then
+    str "Closed under the global context"
+  else
+    let safe_pr_constant env kn =
+      try pr_constant env kn
+      with Not_found ->
+	let mp,_,lab = repr_con kn in
+	str (string_of_mp mp ^ "." ^ Label.to_string lab)
+    in
+    let safe_pr_ltype typ =
+      try str " : " ++ pr_ltype typ
+      with e when Errors.noncritical e -> mt ()
+    in
+    let fold t typ accu =
+      let (v, a, o, tr) = accu in
+      match t with
+      | Variable id ->
+        let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in
+        (var :: v, a, o, tr)
+      | Axiom kn ->
+        let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in
+        (v, ax :: a, o, tr)
+      | Opaque kn ->
+        let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in
+        (v, a, opq :: o, tr)
+      | Transparent kn ->
+        let tran = safe_pr_constant env kn ++ safe_pr_ltype typ in
+        (v, a, o, tran :: tr)
+    in
+    let (vars, axioms, opaque, trans) = 
+      ContextObjectMap.fold fold s ([], [], [], [])
+    in
+    let opt_list title = function
+    | [] -> None
+    | l ->
+      let section =
+        title ++ fnl () ++
+        v 0 (prlist_with_sep fnl (fun s -> s) l) in
+      Some section
+    in
+    let assums = [
+      opt_list (str "Transparent constants:") trans;
+      opt_list (str "Section Variables:") vars;
+      opt_list (str "Axioms:") axioms;
+      opt_list (str "Opaque constants:") opaque;
+    ] in
+    prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
+
+let xor a b = 
+  (a && not b) || (not a && b)
+
+let pr_polymorphic b = 
+  let print = xor (Flags.is_universe_polymorphism ()) b in
+  if print then
+    if b then str"Polymorphic " else str"Monomorphic "
+  else mt ()
+
diff --git a/printing/printer.mli b/printing/printer.mli
new file mode 100644
index 00000000..6b9c7081
--- /dev/null
+++ b/printing/printer.mli
@@ -0,0 +1,177 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+open Globnames
+open Term
+open Context
+open Environ
+open Pattern
+open Evd
+open Proof_type
+open Glob_term
+
+(** These are the entry points for printing terms, context, tac, ... *)
+
+(** Terms *)
+
+val pr_lconstr_env         : env -> evar_map -> constr -> std_ppcmds
+val pr_lconstr             : constr -> std_ppcmds
+val pr_lconstr_goal_style_env : env -> evar_map -> constr -> std_ppcmds
+
+val pr_constr_env          : env -> evar_map -> constr -> std_ppcmds
+val pr_constr              : constr -> std_ppcmds
+val pr_constr_goal_style_env : env -> evar_map -> constr -> std_ppcmds
+
+(** Same, but resilient to [Nametab] errors. Prints fully-qualified
+    names when [shortest_qualid_of_global] has failed. Prints "??"
+    in case of remaining issues (such as reference not in env). *)
+
+val safe_pr_lconstr_env         : env -> evar_map -> constr -> std_ppcmds
+val safe_pr_lconstr             : constr -> std_ppcmds
+
+val safe_pr_constr_env          : env -> evar_map -> constr -> std_ppcmds
+val safe_pr_constr              : constr -> std_ppcmds
+
+
+val pr_open_constr_env     : env -> evar_map -> open_constr -> std_ppcmds
+val pr_open_constr         : open_constr -> std_ppcmds
+
+val pr_open_lconstr_env    : env -> evar_map -> open_constr -> std_ppcmds
+val pr_open_lconstr        : open_constr -> std_ppcmds
+
+val pr_constr_under_binders_env  : env -> evar_map -> constr_under_binders -> std_ppcmds
+val pr_constr_under_binders      : constr_under_binders -> std_ppcmds
+
+val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds
+val pr_lconstr_under_binders     : constr_under_binders -> std_ppcmds
+
+val pr_goal_concl_style_env : env -> evar_map -> types -> std_ppcmds
+val pr_ltype_env           : env -> evar_map -> types -> std_ppcmds
+val pr_ltype               : types -> std_ppcmds
+
+val pr_type_env            : env -> evar_map -> types -> std_ppcmds
+val pr_type                : types -> std_ppcmds
+
+val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> std_ppcmds
+val pr_closed_glob         : closed_glob_constr -> std_ppcmds
+
+val pr_ljudge_env          : env -> evar_map -> unsafe_judgment -> std_ppcmds * std_ppcmds
+val pr_ljudge              : unsafe_judgment -> std_ppcmds * std_ppcmds
+
+val pr_lglob_constr_env      : env -> glob_constr -> std_ppcmds
+val pr_lglob_constr          : glob_constr -> std_ppcmds
+
+val pr_glob_constr_env       : env -> glob_constr -> std_ppcmds
+val pr_glob_constr           : glob_constr -> std_ppcmds
+
+val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> std_ppcmds
+val pr_lconstr_pattern     : constr_pattern -> std_ppcmds
+
+val pr_constr_pattern_env  : env -> evar_map -> constr_pattern -> std_ppcmds
+val pr_constr_pattern      : constr_pattern -> std_ppcmds
+
+val pr_cases_pattern       : cases_pattern -> std_ppcmds
+
+val pr_sort                : evar_map -> sorts -> std_ppcmds
+
+(** Universe constraints *)
+
+val pr_polymorphic         : bool -> std_ppcmds
+val pr_universe_ctx        : Univ.universe_context -> std_ppcmds
+
+(** Printing global references using names as short as possible *)
+
+val pr_global_env          : Id.Set.t -> global_reference -> std_ppcmds
+val pr_global              : global_reference -> std_ppcmds
+
+val pr_constant            : env -> constant -> std_ppcmds
+val pr_existential_key     : evar_map -> existential_key -> std_ppcmds
+val pr_existential         : env -> evar_map -> existential -> std_ppcmds
+val pr_constructor         : env -> constructor -> std_ppcmds
+val pr_inductive           : env -> inductive -> std_ppcmds
+val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds
+
+val pr_pconstant           : env -> pconstant -> std_ppcmds
+val pr_pinductive          : env -> pinductive -> std_ppcmds
+val pr_pconstructor        : env -> pconstructor -> std_ppcmds
+
+
+(** Contexts *)
+
+val pr_context_unlimited   : env -> evar_map -> std_ppcmds
+val pr_ne_context_of       : std_ppcmds -> env -> evar_map -> std_ppcmds
+
+val pr_var_decl            : env -> evar_map -> named_declaration -> std_ppcmds
+val pr_var_list_decl       : env -> evar_map -> named_list_declaration -> std_ppcmds
+val pr_rel_decl            : env -> evar_map -> rel_declaration -> std_ppcmds
+
+val pr_named_context       : env -> evar_map -> named_context -> std_ppcmds
+val pr_named_context_of    : env -> evar_map -> std_ppcmds
+val pr_rel_context         : env -> evar_map -> rel_context -> std_ppcmds
+val pr_rel_context_of      : env -> evar_map -> std_ppcmds
+val pr_context_of          : env -> evar_map -> std_ppcmds
+
+(** Predicates *)
+
+val pr_predicate           : ('a -> std_ppcmds) -> (bool * 'a list) -> std_ppcmds
+val pr_cpred               : Cpred.t -> std_ppcmds
+val pr_idpred              : Id.Pred.t -> std_ppcmds
+val pr_transparent_state   : transparent_state -> std_ppcmds
+
+(** Proofs *)
+
+val pr_goal                : goal sigma -> std_ppcmds
+val pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds
+val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
+val pr_concl               : int -> evar_map -> goal -> std_ppcmds
+
+val pr_open_subgoals       : ?proof:Proof.proof -> unit -> std_ppcmds
+val pr_nth_open_subgoal    : int -> std_ppcmds
+val pr_evar                : evar_map -> (evar * evar_info) -> std_ppcmds
+val pr_evars_int           : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds
+val pr_evars               : evar_map -> evar_info Evar.Map.t -> std_ppcmds
+
+val pr_prim_rule           : prim_rule -> std_ppcmds
+
+(** Emacs/proof general support
+   (emacs_str s) outputs
+    - s if emacs mode,
+    - nothing otherwise.
+    This function was previously used to insert special chars like
+    [(String.make 1 (Char.chr 253))] to parenthesize sub-parts of the
+    proof context for proof by pointing. This part of the code is
+    removed for now because it interacted badly with utf8. We may put
+    it back some day using some xml-like tags instead of special
+    chars. See for example the <prompt> tag in the prompt when in
+    emacs mode. *)
+val emacs_str              : string -> string
+
+(** Backwards compatibility *)
+
+val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
+
+
+(** spiwack: printer function for sets of Environ.assumption.
+            It is used primarily by the Print Assumption command. *)
+val pr_assumptionset :
+  env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds
+
+val pr_goal_by_id : string -> std_ppcmds
+
+type printer_pr = {
+ pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
+ pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
+ pr_goal                : goal sigma -> std_ppcmds;
+};;
+
+val set_printer_pr : printer_pr -> unit
+
+val default_printer_pr : printer_pr
+
diff --git a/printing/printing.mllib b/printing/printing.mllib
new file mode 100644
index 00000000..7b4c71a8
--- /dev/null
+++ b/printing/printing.mllib
@@ -0,0 +1,14 @@
+Genprint
+Pputils
+Ppstyle
+Ppannotation
+Ppconstr
+Ppconstrsig
+Printer
+Pptactic
+Pptacticsig
+Printmod
+Prettyp
+Ppvernac
+Ppvernacsig
+Richprinter
diff --git a/printing/printmod.ml b/printing/printmod.ml
new file mode 100644
index 00000000..295d8aaa
--- /dev/null
+++ b/printing/printmod.ml
@@ -0,0 +1,438 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Term
+open Pp
+open Names
+open Environ
+open Declarations
+open Nameops
+open Globnames
+open Libnames
+open Goptions
+
+(** Note: there is currently two modes for printing modules.
+    - The "short" one, that just prints the names of the fields.
+    - The "rich" one, that also tries to print the types of the fields.
+    The short version used to be the default behavior, but now we print
+    types by default. The following option allows changing this.
+    Technically, the environments in this file are either None in
+    the "short" mode or (Some env) in the "rich" one.
+*)
+
+let short = ref false
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "short module printing";
+      optkey   = ["Short";"Module";"Printing"];
+      optread  = (fun () -> !short) ;
+      optwrite = ((:=) short) }
+
+(** Each time we have to print a non-globally visible structure,
+    we place its elements in a fake fresh namespace. *)
+
+let mk_fake_top =
+  let r = ref 0 in
+  fun () -> incr r; Id.of_string ("FAKETOP"^(string_of_int !r))
+
+module Make (Taggers : sig
+  val tag_definition : std_ppcmds -> std_ppcmds
+  val tag_keyword : std_ppcmds -> std_ppcmds
+end) =
+struct
+
+let def s = Taggers.tag_definition (str s)
+let keyword s = Taggers.tag_keyword (str s)
+
+let get_new_id locals id =
+  let rec get_id l id =
+    let dir = DirPath.make [id] in
+      if not (Nametab.exists_module dir) then
+	id
+      else
+	get_id (id::l) (Namegen.next_ident_away id l)
+  in
+    get_id (List.map snd locals) id
+
+(** Inductive declarations *)
+
+open Termops
+open Reduction
+
+let print_params env sigma params =
+  if List.is_empty params then mt ()
+  else Printer.pr_rel_context env sigma params ++ brk(1,2)
+
+let print_constructors envpar names types =
+  let pc =
+    prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
+      (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar Evd.empty c)
+      (Array.to_list (Array.map2 (fun n t -> (n,t)) names types))
+  in
+  hv 0 (str "  " ++ pc)
+
+let build_ind_type env mip =
+  Inductive.type_of_inductive env mip
+
+let print_one_inductive env mib ((_,i) as ind) =
+  let u = if mib.mind_polymorphic then 
+      Univ.UContext.instance mib.mind_universes 
+    else Univ.Instance.empty in
+  let mip = mib.mind_packets.(i) in
+  let params = Inductive.inductive_paramdecls (mib,u) in
+  let args = extended_rel_list 0 params in
+  let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
+  let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
+  let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
+  let envpar = push_rel_context params env in
+  hov 0 (
+    pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++
+    str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++
+  brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
+
+let print_mutual_inductive env mind mib =
+  let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
+  in
+  let keyword =
+    let open Decl_kinds in
+    match mib.mind_finite with
+    | Finite -> "Inductive"
+    | BiFinite -> "Variant"
+    | CoFinite -> "CoInductive"
+  in
+  hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++
+    def keyword ++ spc () ++
+    prlist_with_sep (fun () -> fnl () ++ str"  with ")
+      (print_one_inductive env mib) inds ++
+      Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
+
+let get_fields =
+  let rec prodec_rec l subst c =
+    match kind_of_term c with
+    | Prod (na,t,c) ->
+        let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in
+        prodec_rec ((id,true,Vars.substl subst t)::l) (mkVar id::subst) c
+    | LetIn (na,b,_,c) ->
+        let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in
+        prodec_rec ((id,false,Vars.substl subst b)::l) (mkVar id::subst) c
+    | _               -> List.rev l
+  in
+  prodec_rec [] []
+
+let print_record env mind mib =
+  let u = 
+    if mib.mind_polymorphic then 
+      Univ.UContext.instance mib.mind_universes 
+    else Univ.Instance.empty 
+  in
+  let mip = mib.mind_packets.(0) in
+  let params = Inductive.inductive_paramdecls (mib,u) in
+  let args = extended_rel_list 0 params in
+  let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
+  let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
+  let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
+  let fields = get_fields cstrtype in
+  let envpar = push_rel_context params env in
+  let keyword =
+    let open Decl_kinds in
+    match mib.mind_finite with
+    | BiFinite -> "Record"
+    | Finite -> "Inductive"
+    | CoFinite -> "CoInductive"
+  in
+  hov 0 (
+    hov 0 (
+      Printer.pr_polymorphic mib.mind_polymorphic ++
+      def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++
+      print_params env Evd.empty params ++
+      str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++
+      str ":= " ++ pr_id mip.mind_consnames.(0)) ++
+    brk(1,2) ++
+    hv 2 (str "{ " ++
+      prlist_with_sep (fun () -> str ";" ++ brk(2,0))
+        (fun (id,b,c) ->
+          pr_id id ++ str (if b then " : " else " := ") ++
+          Printer.pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++
+      Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
+
+let pr_mutual_inductive_body env mind mib =
+  if mib.mind_record <> None && not !Flags.raw_print then
+    print_record env mind mib
+  else
+    print_mutual_inductive env mind mib
+
+(** Modpaths *)
+
+let rec print_local_modpath locals = function
+  | MPbound mbid -> pr_id (Util.List.assoc_f MBId.equal mbid locals)
+  | MPdot(mp,l) ->
+      print_local_modpath locals mp ++ str "." ++ pr_lab l
+  | MPfile _ -> raise Not_found
+
+let print_modpath locals mp =
+  try (* must be with let because streams are lazy! *)
+    let qid = Nametab.shortest_qualid_of_module mp in
+      pr_qualid qid
+  with
+    | Not_found -> print_local_modpath locals mp
+
+let print_kn locals kn =
+  try
+    let qid = Nametab.shortest_qualid_of_modtype kn in
+      pr_qualid qid
+  with
+      Not_found ->
+	try
+	  print_local_modpath locals kn
+	with
+	    Not_found -> print_modpath locals kn
+
+let nametab_register_dir mp =
+  let id = mk_fake_top () in
+  let dir = DirPath.make [id] in
+  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty)))
+
+(** Nota: the [global_reference] we register in the nametab below
+    might differ from internal ones, since we cannot recreate here
+    the canonical part of constant and inductive names, but only
+    the user names. This works nonetheless since we search now
+    [Nametab.the_globrevtab] modulo user name. *)
+
+let nametab_register_body mp dir (l,body) =
+  let push id ref =
+    Nametab.push (Nametab.Until (1+List.length (DirPath.repr dir)))
+      (make_path dir id) ref
+  in
+  match body with
+    | SFBmodule _ -> () (* TODO *)
+    | SFBmodtype _ -> () (* TODO *)
+    | SFBconst _ ->
+      push (Label.to_id l) (ConstRef (Constant.make2 mp l))
+    | SFBmind mib ->
+      let mind = MutInd.make2 mp l in
+      Array.iteri
+	(fun i mip ->
+	  push mip.mind_typename (IndRef (mind,i));
+	  Array.iteri (fun j id -> push id (ConstructRef ((mind,i),j+1)))
+	    mip.mind_consnames)
+	mib.mind_packets
+
+let nametab_register_module_body mp struc =
+  (* If [mp] is a globally visible module, we simply import it *)
+  try Declaremods.really_import_module mp
+  with Not_found ->
+    (* Otherwise we try to emulate an import by playing with nametab *)
+    nametab_register_dir mp;
+    List.iter (nametab_register_body mp DirPath.empty) struc
+
+let get_typ_expr_alg mtb = match mtb.mod_type_alg with
+  | Some (NoFunctor me) -> me
+  | _ -> raise Not_found
+
+let nametab_register_modparam mbid mtb =
+  match mtb.mod_type with
+  | MoreFunctor _ -> () (* functorial param : nothing to register *)
+  | NoFunctor struc ->
+    (* We first try to use the algebraic type expression if any,
+       via a Declaremods function that converts back to module entries *)
+    try
+      Declaremods.process_module_binding mbid (get_typ_expr_alg mtb)
+    with e when Errors.noncritical e ->
+      (* Otherwise, we try to play with the nametab ourselves *)
+      let mp = MPbound mbid in
+      let dir = DirPath.make [MBId.to_id mbid] in
+      nametab_register_dir mp;
+      List.iter (nametab_register_body mp dir) struc
+
+let print_body is_impl env mp (l,body) =
+  let name = str (Label.to_string l) in
+  hov 2 (match body with
+    | SFBmodule _ -> keyword "Module" ++ spc () ++ name
+    | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
+    | SFBconst cb ->
+      (match cb.const_body with
+	| Def _ -> def "Definition" ++ spc ()
+	| OpaqueDef _ when is_impl -> def "Theorem" ++ spc ()
+	| _ -> def "Parameter" ++ spc ()) ++ name ++
+      (match env with
+	  | None -> mt ()
+	  | Some env ->
+	    str " :" ++ spc () ++
+	    hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *)
+		     (Typeops.type_of_constant_type env cb.const_type)) ++
+	    (match cb.const_body with
+	      | Def l when is_impl ->
+		spc () ++
+		hov 2 (str ":= " ++
+		       Printer.pr_lconstr_env env Evd.empty (Mod_subst.force_constr l))
+	      | _ -> mt ()) ++ str "." ++
+	    Printer.pr_universe_ctx cb.const_universes)
+    | SFBmind mib ->
+      try
+	let env = Option.get env in
+	pr_mutual_inductive_body env (MutInd.make2 mp l) mib
+      with e when Errors.noncritical e ->
+        let keyword =
+          let open Decl_kinds in
+          match mib.mind_finite with
+          | Finite -> def "Inductive"
+          | BiFinite -> def "Variant"
+          | CoFinite -> def "CoInductive"
+        in
+	keyword ++ spc () ++ name)
+
+let print_struct is_impl env mp struc =
+  prlist_with_sep spc (print_body is_impl env mp) struc
+
+let print_structure is_type env mp locals struc =
+  let env' = Option.map
+    (Modops.add_structure mp struc Mod_subst.empty_delta_resolver) env in
+  nametab_register_module_body mp struc;
+  let kwd = if is_type then "Sig" else "Struct" in
+  hv 2 (keyword kwd ++ spc () ++ print_struct false env' mp struc ++
+	brk (1,-2) ++ keyword "End")
+
+let rec flatten_app mexpr l = match mexpr with
+  | MEapply (mexpr, arg) -> flatten_app mexpr (arg::l)
+  | MEident mp -> mp::l
+  | MEwith _ -> assert false
+
+let rec print_typ_expr env mp locals mty =
+  match mty with
+  | MEident kn -> print_kn locals kn
+  | MEapply _ ->
+      let lapp = flatten_app mty [] in
+      let fapp = List.hd lapp in
+      let mapp = List.tl lapp in
+      hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++
+		 prlist_with_sep spc (print_modpath locals) mapp ++ str")")
+  | MEwith(me,WithDef(idl,c))->
+      let env' = None in (* TODO: build a proper environment if env <> None *)
+      let s = String.concat "." (List.map Id.to_string idl) in
+      hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc()
+             ++ def "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
+  | MEwith(me,WithMod(idl,mp))->
+      let s = String.concat "." (List.map Id.to_string idl) in
+      hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++
+             keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
+
+let print_mod_expr env mp locals = function
+  | MEident mp -> print_modpath locals mp
+  | MEapply _ as me ->
+      let lapp = flatten_app me [] in
+      hov 3
+        (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
+  | MEwith _ -> assert false (* No 'with' syntax for modules *)
+
+let rec print_functor fty fatom is_type env mp locals = function
+  |NoFunctor me -> fatom is_type env mp locals me
+  |MoreFunctor (mbid,mtb1,me2) ->
+      nametab_register_modparam mbid mtb1;
+      let mp1 = MPbound mbid in
+      let pr_mtb1 = fty env mp1 locals mtb1 in
+      let env' = Option.map (Modops.add_module_type mp1 mtb1) env in
+      let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in
+      let kwd = if is_type then "Funsig" else "Functor" in
+      hov 2
+        (keyword kwd ++ spc () ++
+	 str "(" ++ pr_id (MBId.to_id mbid) ++ str ":" ++ pr_mtb1 ++ str ")" ++
+	 spc() ++ print_functor fty fatom is_type env' mp locals' me2)
+
+let rec print_expression x =
+  print_functor
+    print_modtype
+    (function true -> print_typ_expr | false -> print_mod_expr) x
+
+and print_signature x =
+  print_functor print_modtype print_structure x
+
+and print_modtype env mp locals mtb = match mtb.mod_type_alg with
+  | Some me -> print_expression true env mp locals me
+  | None -> print_signature true env mp locals mtb.mod_type
+
+let rec printable_body dir =
+  let dir = pop_dirpath dir in
+    DirPath.is_empty dir ||
+    try
+      match Nametab.locate_dir (qualid_of_dirpath dir) with
+	  DirOpenModtype _ -> false
+	| DirModule _ | DirOpenModule _ -> printable_body dir
+	| _ -> true
+    with
+	Not_found -> true
+
+(** Since we might play with nametab above, we should reset to prior
+    state after the printing *)
+
+let print_expression' is_type env mp me =
+  States.with_state_protection
+    (fun e -> eval_ppcmds (print_expression is_type env mp [] e)) me
+
+let print_signature' is_type env mp me =
+  States.with_state_protection
+    (fun e -> eval_ppcmds (print_signature is_type env mp [] e)) me
+
+let unsafe_print_module env mp with_body mb =
+  let name = print_modpath [] mp in
+  let pr_equals = spc () ++ str ":= " in
+  let body = match with_body, mb.mod_expr with
+    | false, _
+    | true, Abstract -> mt()
+    | _, Algebraic me -> pr_equals ++ print_expression' false env mp me
+    | _, Struct sign -> pr_equals ++ print_signature' false env mp sign
+    | _, FullStruct -> pr_equals ++ print_signature' false env mp mb.mod_type
+  in
+  let modtype = match mb.mod_expr, mb.mod_type_alg with
+    | FullStruct, _ -> mt ()
+    | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' true env mp ty
+    | _, _ -> brk (1,1) ++ str": " ++ print_signature' true env mp mb.mod_type
+  in
+  hv 0 (keyword "Module" ++ spc () ++ name ++ modtype ++ body)
+
+exception ShortPrinting
+
+let print_module with_body mp =
+  let me = Global.lookup_module mp in
+  try
+    if !short then raise ShortPrinting;
+    unsafe_print_module (Some (Global.env ())) mp with_body me ++ fnl ()
+  with e when Errors.noncritical e ->
+    unsafe_print_module None mp with_body me ++ fnl ()
+
+let print_modtype kn =
+  let mtb = Global.lookup_modtype kn in
+  let name = print_kn [] kn in
+  hv 1
+    (keyword "Module Type" ++ spc () ++ name ++ str " =" ++ spc () ++
+     (try
+	if !short then raise ShortPrinting;
+	print_signature' true (Some (Global.env ())) kn mtb.mod_type
+      with e when Errors.noncritical e ->
+	print_signature' true None kn mtb.mod_type))
+
+end
+
+module Tag =
+struct
+  let definition =
+    let style = Terminal.make ~bold:true ~fg_color:`LIGHT_RED () in
+    Ppstyle.make ~style ["module"; "definition"]
+  let keyword =
+    let style = Terminal.make ~bold:true () in
+    Ppstyle.make ~style ["module"; "keyword"]
+end
+
+include Make(struct
+  let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
+  let tag_definition s = tag Tag.definition s
+  let tag_keyword s = tag Tag.keyword s
+end)
diff --git a/printing/printmod.mli b/printing/printmod.mli
new file mode 100644
index 00000000..bea47534
--- /dev/null
+++ b/printing/printmod.mli
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+
+(** false iff the module is an element of an open module type *)
+val printable_body : DirPath.t -> bool
+
+include Printmodsig.Pp
diff --git a/printing/printmodsig.mli b/printing/printmodsig.mli
new file mode 100644
index 00000000..5d0d4ab0
--- /dev/null
+++ b/printing/printmodsig.mli
@@ -0,0 +1,17 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+
+module type Pp =
+sig
+  val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds
+  val print_module : bool -> module_path -> std_ppcmds
+  val print_modtype : module_path -> std_ppcmds
+end
diff --git a/printing/richprinter.ml b/printing/richprinter.ml
new file mode 100644
index 00000000..d71dc82d
--- /dev/null
+++ b/printing/richprinter.ml
@@ -0,0 +1,26 @@
+open Richpp
+
+module RichppConstr = Ppconstr.Richpp
+module RichppVernac = Ppvernac.Richpp
+module RichppTactic = Pptactic.Richpp
+
+type rich_pp =
+    string
+    * Ppannotation.t Richpp.located Xml_datatype.gxml
+    * Xml_datatype.xml
+
+let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag
+
+let make_richpp pr ast =
+  let raw_pp, rich_pp =
+    rich_pp get_annotations (pr ast)
+  in
+  let xml = Ppannotation.(
+    xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp
+  )
+  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
new file mode 100644
index 00000000..c67d52c0
--- /dev/null
+++ b/printing/richprinter.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This module provides an entry point to "rich" pretty-printers that
+    produce pretty-printing as done by {!Printer} but with additional
+    annotations represented as a semi-structured document.
+
+    To understand what are these annotations and how they are represented
+    as standard XML attributes, please refer to {!Ppannotation}.
+
+    In addition to these annotations, each node of the semi-structured
+    document contains a [startpos] and an [endpos] attribute that
+    relate this node to the raw pretty-printing.
+    Please refer to {!Richpp} for more details. *)
+
+(** A rich pretty-print is composed of: *)
+type rich_pp =
+    (** - a raw pretty-print ; *)
+    string
+
+    (** - a generalized semi-structured document whose attributes are
+        annotations ; *)
+    * Ppannotation.t Richpp.located Xml_datatype.gxml
+
+    (** - an XML document, representing annotations as usual textual
+        XML attributes. *)
+    * Xml_datatype.xml
+
+(** [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