From dfac5aa2285de5b89f08ada3c30c0a1594737440 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 7 Sep 2016 18:02:52 +0200
Subject: Making Vernacexpr independent from Tacexpr.

---
 intf/genredexpr.mli | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'intf/genredexpr.mli')

diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
index 2df79673ad..16f0c0c92a 100644
--- a/intf/genredexpr.mli
+++ b/intf/genredexpr.mli
@@ -8,6 +8,8 @@
 
 (** Reduction expressions *)
 
+open Names
+
 (** The parsing produces initially a list of [red_atom] *)
 
 type 'a red_atom =
@@ -50,5 +52,15 @@ type ('a,'b,'c) red_expr_gen =
 type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
   | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of (Loc.t * Names.Id.t) * 'a
+  | ConstrContext of (Loc.t * Id.t) * 'a
   | ConstrTypeOf of 'a
+
+open Libnames
+open Constrexpr
+open Misctypes
+
+type r_trm = constr_expr
+type r_pat = constr_pattern_expr
+type r_cst = reference or_by_notation
+
+type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
-- 
cgit v1.2.3