From 7f56dfb365e58f8dbb1db99faecec2a126bab0e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Nov 2014 18:58:18 +0100
Subject: Plug the dynamic tags in the Richpp mechanism.

---
 printing/richprinter.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'printing/richprinter.ml')

diff --git a/printing/richprinter.ml b/printing/richprinter.ml
index d27b7c3736..d71dc82d50 100644
--- a/printing/richprinter.ml
+++ b/printing/richprinter.ml
@@ -1,19 +1,19 @@
 open Richpp
 
-module Indexer = Indexer (struct type t = Ppannotation.t end)
-
-module RichppConstr = Ppconstr.Richpp (Indexer)
-module RichppVernac = Ppvernac.Richpp (Indexer)
-module RichppTactic = Pptactic.Richpp (Indexer)
+module RichppConstr = Ppconstr.Richpp
+module RichppVernac = Ppvernac.Richpp
+module RichppTactic = Pptactic.Richpp
 
 type rich_pp =
     string
     * 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 raw_pp, rich_pp =
-    rich_pp Indexer.get_annotations (fun () -> pr ast)
+    rich_pp get_annotations (pr ast)
   in
   let xml = Ppannotation.(
     xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp
-- 
cgit v1.2.3