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
---
 proofs/tacexpr.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index af3eec9812..1dc822a27c 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -307,10 +307,10 @@ type closed_raw_generic_argument =
     (constr_expr,raw_tactic_expr) generic_argument
 
 type 'a raw_abstract_argument_type =
-    ('a,constr_expr,raw_tactic_expr) abstract_argument_type
+    ('a,rlevel,raw_tactic_expr) abstract_argument_type
 
 type 'a glob_abstract_argument_type =
-    ('a,rawconstr_and_expr,glob_tactic_expr) abstract_argument_type
+    ('a,glevel,glob_tactic_expr) abstract_argument_type
 
 type open_generic_argument =
     (Term.constr,glob_tactic_expr) generic_argument
-- 
cgit v1.2.3