From 9024a91b59b9ecfb94e68b3748f2a9a66adcf515 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 21 Jun 2013 12:36:19 +0000
Subject: Cutting the dependency of Genarg in constr_expr, glob_constr related
 types. This will ultimately allow putting genargs into these ASTs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/extraargs.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/extraargs.mli')

diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index cd4d777d6..1367f7032 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -26,7 +26,7 @@ val occurrences_of : int list -> Locus.occurrences
 
 val wit_glob :
   (constr_expr,
-  Genarg.glob_constr_and_expr,
+  Tacexpr.glob_constr_and_expr,
   Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
 val glob : constr_expr Pcoq.Gram.entry
 
-- 
cgit v1.2.3