[pp] Remove unused printing tagging infrastructure.

Applications of it were not clear/unproven, it made printers more
complex (as they needed to be functors) and as it lacked examples it
confused some people.

The printers now tag unconditionally, it is up to the backends to
interpreted the tags.

Tagging (and indeed the notion of rich document) should be reworked in
a follow-up patch, so they are in sync, but this is a first step.

Tested, test-suite passes.

Notes:

- We remove the `Richprinter` module. It was only used in the
  `annotate` IDE protocol call, its output was identical to the normal
  printer (or even inconsistent if taggers were not kept manually in
  sync).

- Note that Richpp didn't need a single change. In particular, its
  main API entry point `Richpp.rich_pp` is not used by anyone.

17 files changed, 230 insertions, 562 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 8a1f8c638..0cb8d377f 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -114,11 +114,8 @@ let annotate phrase =
     let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
     Vernac.parse_sentence (pa,None)
   in
-  let (_, xml) =
-    Richprinter.richpp_vernac ast
-  in
-  xml
-
+  Richpp.repr (Richpp.richpp_of_pp (Ppvernac.pr_vernac ast))
+    
 (** Goal display *)
 
 let hyp_next_tac sigma env decl =
diff --git a/ide/richprinter.ml b/ide/richprinter.ml
deleted file mode 100644
index 995cef1ac..000000000
--- a/ide/richprinter.ml
+++ /dev/null
@@ -1,23 +0,0 @@
-open Richpp
-
-module RichppConstr = Ppconstr.Richpp
-module RichppVernac = Ppvernac.Richpp
-
-type rich_pp =
-    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 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
-  (rich_pp, xml)
-
-let richpp_vernac = make_richpp RichppVernac.pr_vernac
-let richpp_constr = make_richpp RichppConstr.pr_constr_expr
diff --git a/ide/richprinter.mli b/ide/richprinter.mli
deleted file mode 100644
index c9e84e3eb..000000000
--- a/ide/richprinter.mli
+++ /dev/null
@@ -1,36 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \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 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
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6f4ef37b4..9dacce28d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -27,6 +27,33 @@ open Pputils
 open Ppconstr
 open Printer
 
+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
+
+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_atomic_tactic_expr      = do_not_tag
+
 let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
 type 'a grammar_tactic_prod_item_expr =
@@ -64,30 +91,6 @@ type 'a extra_genarg_printer =
     (tolerability -> Val.t -> std_ppcmds) ->
     'a -> std_ppcmds
 
-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_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)
 
@@ -1206,37 +1209,6 @@ module Make
 
   let pr_atomic_tactic env = pr_atomic_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_atomic_tactic_expr      = do_not_tag
-end)
-
 let declare_extra_genarg_pprule wit
   (f : 'a raw_extra_genarg_printer)
   (g : 'b glob_extra_genarg_printer)
@@ -1338,22 +1310,3 @@ let () =
   let pr_unit _ _ _ () = str "()" in
   let printer _ _ prtac = prtac (0, E) in
   declare_extra_genarg_pprule wit_ltac printer printer pr_unit
-
-module Richpp = struct
-
-  include Make (Ppconstr.Richpp) (struct
-    open Ppannotation
-    open Genarg
-    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 (AGlbGenArg (in_gen (glbwit wit_ltac) e))
-    let tag_glob_atomic_tactic_expr   = do_not_tag
-    let tag_raw_tactic_expr         e = tag (ARawGenArg (in_gen (rawwit wit_ltac) e))
-    let tag_raw_atomic_tactic_expr    = do_not_tag
-    let tag_atomic_tactic_expr        = do_not_tag
-  end)
-
-end
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 86e3ea548..43e22dba3 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -13,6 +13,8 @@ open Pp
 open Genarg
 open Geninterp
 open Names
+open Misctypes
+open Environ
 open Constrexpr
 open Tacexpr
 open Ppextend
@@ -54,14 +56,66 @@ type pp_tactic = {
 
 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
+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_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_in_clause :
+  ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
+val pr_clauses :  bool option ->
+  ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
+val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
+
+val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
+
+val pr_raw_extend: env -> int ->
+  ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
+
+val pr_glob_extend: env -> int ->
+  ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
+
+val pr_extend :
+  (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
+
+val pr_alias_key : Names.KerName.t -> std_ppcmds
+
+val pr_alias : (Val.t -> std_ppcmds) ->
+  int -> Names.KerName.t -> Val.t 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_atomic_tactic : env -> atomic_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
+
+val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
+
+val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+  ('b, 'a) match_rule -> std_ppcmds
+
+val pr_value : tolerability -> Val.t -> std_ppcmds
 
-(** 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
 
 val ltop : tolerability
diff --git a/plugins/ltac/pptacticsig.mli b/plugins/ltac/pptacticsig.mli
deleted file mode 100644
index 74ddd377a..000000000
--- a/plugins/ltac/pptacticsig.mli
+++ /dev/null
@@ -1,81 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pp
-open Genarg
-open Geninterp
-open Tacexpr
-open Ppextend
-open Environ
-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_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
-
-  val pr_in_clause :
-    ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
-
-  val pr_clauses :  bool option ->
-    ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
-
-  val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
-
-  val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
-
-  val pr_raw_extend: env -> int ->
-    ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
-
-  val pr_glob_extend: env -> int ->
-    ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
-
-  val pr_extend :
-    (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
-
-  val pr_alias_key : Names.KerName.t -> std_ppcmds
-
-  val pr_alias : (Val.t -> std_ppcmds) ->
-    int -> Names.KerName.t -> Val.t list -> std_ppcmds
-
-  val pr_alias_key : Names.KerName.t -> 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_atomic_tactic : env -> atomic_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
-
-  val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
-
-  val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
-    ('b, 'a) match_rule -> std_ppcmds
-
-  val pr_value : tolerability -> Val.t -> std_ppcmds
-
-end
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
deleted file mode 100644
index 726c0ffcf..000000000
--- a/printing/ppannotation.ml
+++ /dev/null
@@ -1,33 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \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 Genarg
-
-type t =
-  | AKeyword
-  | AUnparsing            of unparsing
-  | AConstrExpr           of constr_expr
-  | AVernac               of vernac_expr
-  | AGlbGenArg            of glob_generic_argument
-  | ARawGenArg            of raw_generic_argument
-
-let tag_of_annotation = function
-  | AKeyword                -> "keyword"
-  | AUnparsing _            -> "unparsing"
-  | AConstrExpr _           -> "constr_expr"
-  | AVernac _               -> "vernac_expr"
-  | AGlbGenArg _            -> "glob_generic_argument"
-  | ARawGenArg _            -> "raw_generic_argument"
-
-let attributes_of_annotation a =
-  []
-
-let tag = Pp.Tag.create "ppannotation"
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
deleted file mode 100644
index b0e0facef..000000000
--- a/printing/ppannotation.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \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 Genarg
-
-type t =
-  | AKeyword
-  | AUnparsing            of unparsing
-  | AConstrExpr           of constr_expr
-  | AVernac               of vernac_expr
-  | AGlbGenArg            of glob_generic_argument
-  | ARawGenArg            of raw_generic_argument
-
-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
index 80ddd669f..b16384c60 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -21,18 +21,49 @@ 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
+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
+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
+
 
   let keyword s = tag_keyword (str s)
   let sep_v = fun _ -> str"," ++ spc()
@@ -764,86 +795,3 @@ end) = struct
 
   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
-
-let split_token tag s =
-  let len = String.length s in
-  let rec parse_string off i =
-    if Int.equal i len then
-      if Int.equal off i then mt () else tag (str (String.sub s off (i - off)))
-    else if s.[i] == ' ' then
-      if Int.equal off i then parse_space 1 (succ i)
-      else tag (str (String.sub s off (i - off))) ++ parse_space 1 (succ i)
-    else parse_string off (succ i)
-  and parse_space spc i =
-    if Int.equal i len then str (String.make spc ' ')
-    else if s.[i] == ' ' then parse_space (succ spc) (succ i)
-    else str (String.make spc ' ') ++ parse_string i (succ i)
-  in
-  parse_string 0 0
-
-(** 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 -> fun _ -> split_token (fun pp -> tag Tag.notation pp) s
-    | _ -> 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
index 0241633c6..a0106837a 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -11,11 +11,85 @@
 
 (** The default pretty-printers produce {!Pp.std_ppcmds} that are
     interpreted as raw strings. *)
-include Ppconstrsig.Pp
+open Loc
+open Pp
+open Libnames
+open Constrexpr
+open Names
+open Misctypes
 
-(** 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}. *)
+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
 
-module Richpp : Ppconstrsig.Pp
+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_level : glob_level -> 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_record_body : (reference * constr_expr) list -> 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
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
deleted file mode 100644
index 3de0d805c..000000000
--- a/printing/ppconstrsig.mli
+++ /dev/null
@@ -1,95 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \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
-
-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_level : glob_level -> 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_record_body : (reference * constr_expr) list -> 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/ppvernac.ml b/printing/ppvernac.ml
index ff72be90c..78ef4d4ba 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -19,17 +19,12 @@ open Constrexpr
 open Constrexpr_ops
 open Decl_kinds
 
-module Make
-  (Ppconstr : Ppconstrsig.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
 
+  let do_not_tag _ x = x
+  let tag_keyword = do_not_tag ()
+  let tag_vernac  = do_not_tag
+
   let keyword s = tag_keyword (str s)
 
   let pr_constr = pr_constr_expr
@@ -526,7 +521,7 @@ module Make
   let pr_using e = str (Proof_using.to_string e)
 
   let rec pr_vernac_body v =
-    let return = Taggers.tag_vernac v in
+    let return = tag_vernac v in
     match v with
       | VernacPolymorphic (poly, v) ->
         let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in
@@ -1244,23 +1239,3 @@ module Make
   let pr_vernac v =
     try pr_vernac_body v ++ sep_end v
     with e -> CErrors.print e
-
-end
-
-include Make (Ppconstr) (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)
-    (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
index d3d4a5ceb..836b05e0e 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -9,12 +9,11 @@
 (** 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
+(** Prints a fixpoint body *)
+val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds
 
-(** 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
+(** 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
diff --git a/printing/ppvernacsig.mli b/printing/ppvernacsig.mli
deleted file mode 100644
index 5e5e4bcf4..000000000
--- a/printing/ppvernacsig.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-module type Pp = sig
-
-  (** Prints a fixpoint body *)
-  val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds
-
-  (** 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/printing.mllib b/printing/printing.mllib
index b0141b6d3..86b68d8fb 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -1,6 +1,5 @@
 Genprint
 Pputils
-Ppannotation
 Ppconstr
 Printer
 Printmod
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 7f7d34392..f3079d5b6 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -6,9 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Names
 
 (** false iff the module is an element of an open module type *)
 val printable_body : DirPath.t -> bool
 
-include Printmodsig.Pp
+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
diff --git a/printing/printmodsig.mli b/printing/printmodsig.mli
deleted file mode 100644
index f71fffdce..000000000
--- a/printing/printmodsig.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \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