From 97c05d64e69308ee2d51bb6b82957016efba7273 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 7 Jun 2006 16:59:05 +0000
Subject: Correction trou de subject-reduction de create_arg dans genarg.mli

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8917 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/g_subtac.ml4 | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'contrib')

diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 2f47608c10..55e60199f4 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -49,11 +49,11 @@ GEXTEND Gram
     ;
   END
 
-type gallina_loc_argtype = (Vernacexpr.vernac_expr located, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
+type ('a,'b) gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a, 'b) Genarg.abstract_argument_type
 
-let (wit_subtac_gallina_loc : gallina_loc_argtype),
-  (globwit_subtac_gallina_loc : gallina_loc_argtype),
-  (rawwit_subtac_gallina_loc : gallina_loc_argtype) =
+let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_argtype),
+  (globwit_subtac_gallina_loc : (Genarg.glevel, Tacexpr.glob_tactic_expr) gallina_loc_argtype),
+  (rawwit_subtac_gallina_loc : (Genarg.rlevel, Tacexpr.raw_tactic_expr) gallina_loc_argtype) =
   Genarg.create_arg "subtac_gallina_loc"
 
 VERNAC COMMAND EXTEND Subtac
-- 
cgit v1.2.3