[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.

3 files changed, 89 insertions, 163 deletions

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6f4ef37b44..9dacce28d5 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 86e3ea5484..43e22dba3f 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 74ddd377ad..0000000000
--- 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