From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 ide/richprinter.ml | 24 ------------------------
 1 file changed, 24 deletions(-)
 delete mode 100644 ide/richprinter.ml

(limited to 'ide/richprinter.ml')

diff --git a/ide/richprinter.ml b/ide/richprinter.ml
deleted file mode 100644
index 5f39f36e..00000000
--- a/ide/richprinter.ml
+++ /dev/null
@@ -1,24 +0,0 @@
-open Richpp
-
-module RichppConstr = Ppconstr.Richpp
-module RichppVernac = Ppvernac.Richpp
-module RichppTactic = Pptactic.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
-- 
cgit v1.2.3