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

1 files changed, 80 insertions, 6 deletions

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