From 6f123367027055dbefd9aec9ab2a8bc62f6c32ed Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 15 Sep 2016 19:21:45 +0200
Subject: Made Ppanotation Ltac-agnostic.

---
 ltac/pptactic.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'ltac')

diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index dc2676bf4b..271ed12d52 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -1329,16 +1329,17 @@ 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 (AGlobTacticExpr e)
-    let tag_glob_atomic_tactic_expr a = tag (AGlobAtomicTacticExpr a)
-    let tag_raw_tactic_expr         e = tag (ARawTacticExpr e)
-    let tag_raw_atomic_tactic_expr  a = tag (ARawAtomicTacticExpr a)
-    let tag_atomic_tactic_expr      a = tag (AAtomicTacticExpr a)
+    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
-- 
cgit v1.2.3