From 63d36d429edd2e85cbebe69f66e8949b25b46c70 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Aug 2017 18:32:38 +0200
Subject: Rolling our own generic arguments.

---
 src/tac2expr.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/tac2expr.mli')

diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 0b02ba2656..ccff8e7756 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -104,7 +104,7 @@ type raw_tacexpr =
 | CTacRec of Loc.t * raw_recexpr
 | CTacPrj of Loc.t * raw_tacexpr * ltac_projection or_relid
 | CTacSet of Loc.t * raw_tacexpr * ltac_projection or_relid * raw_tacexpr
-| CTacExt of Loc.t * raw_generic_argument
+| CTacExt : Loc.t * ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr
 
 and raw_taccase = raw_patexpr * raw_tacexpr
 
@@ -132,7 +132,7 @@ type glb_tacexpr =
 | GTacSet of type_constant * glb_tacexpr * int * glb_tacexpr
 | GTacOpn of ltac_constructor * glb_tacexpr list
 | GTacWth of glb_tacexpr open_match
-| GTacExt of glob_generic_argument
+| GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr
 | GTacPrm of ml_tactic_name * glb_tacexpr list
 
 (** {5 Parsing & Printing} *)
-- 
cgit v1.2.3