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
---
 parsing/pcoq.mli    | 2 +-
 parsing/pptactic.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 46ecd11d24..690810d8ab 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -77,7 +77,7 @@ val force_entry_type :
 
 val create_constr_entry :
   string * gram_universe -> string -> constr_expr Gram.Entry.e
-val create_generic_entry : string -> ('a, constr_expr,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e
+val create_generic_entry : string -> ('a, rlevel,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e
 val get_generic_entry : string -> grammar_object Gram.Entry.e
 val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument_type
 
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 2f86ac94cf..f18bcf414a 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -127,7 +127,7 @@ let rec pr_message_token prid = function
   | MsgInt n -> int n
   | MsgIdent id -> prid id
 
-let rec pr_raw_generic prc prlc prtac prref x =
+let rec pr_raw_generic prc prlc prtac prref (x:(Genarg.rlevel, Tacexpr.raw_tactic_expr) Genarg.generic_argument) =
   match Genarg.genarg_tag x with
   | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false")
   | IntArgType -> pr_arg int (out_gen rawwit_int x)
-- 
cgit v1.2.3