[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, 2 insertions, 64 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