Suppression du type 'tac dans les abstract_argument_type: devenu inutile

suite à l'adoption du modèle rlevel,glevel,tlevel et au passage des 
wit_tactic en types créés dynamiquement (révisions 8917 et 8926).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9393 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 25 insertions, 26 deletions

diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index b0f997d24..a79727539 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, rlevel,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e
+val create_generic_entry : string -> ('a, rlevel) 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
 
@@ -85,33 +85,33 @@ val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument
 
 val tactic_main_level : int
 
-val rawwit_tactic : int -> (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic : int -> (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic : int -> (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic : int -> (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic : int -> (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic : int -> (glob_tactic_expr,tlevel) abstract_argument_type
 
-val rawwit_tactic0 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic0 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic0 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic0 : (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic0 : (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic0 : (glob_tactic_expr,tlevel) abstract_argument_type
 
-val rawwit_tactic1 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic1 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic1 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic1 : (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic1 : (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic1 : (glob_tactic_expr,tlevel) abstract_argument_type
 
-val rawwit_tactic2 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic2 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic2 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic2 : (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic2 : (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic2 : (glob_tactic_expr,tlevel) abstract_argument_type
 
-val rawwit_tactic3 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic3 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic3 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic3 : (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic3 : (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic3 : (glob_tactic_expr,tlevel) abstract_argument_type
 
-val rawwit_tactic4 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic4 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic4 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic4 : (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic4 : (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic4 : (glob_tactic_expr,tlevel) abstract_argument_type
 
-val rawwit_tactic5 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic5 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic5 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic5 : (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic5 : (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic5 : (glob_tactic_expr,tlevel) abstract_argument_type
 
 val is_tactic_genarg : argument_type -> bool
 
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 451313be5..ebf4b5ad1 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -129,7 +129,7 @@ let rec pr_message_token prid = function
 
 let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s)
 
-let rec pr_raw_generic prc prlc prtac prref (x:(Genarg.rlevel, Tacexpr.raw_tactic_expr) Genarg.generic_argument) =
+let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel 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)
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 7b546b290..993f1ae62 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -58,9 +58,8 @@ val pr_raw_generic :
   (constr_expr -> std_ppcmds) ->
   (constr_expr -> std_ppcmds) ->
   (tolerability -> raw_tactic_expr -> std_ppcmds) ->
-  (Libnames.reference -> std_ppcmds) ->
-    (constr_expr, raw_tactic_expr) generic_argument ->
-      std_ppcmds
+  (Libnames.reference -> std_ppcmds) -> constr_expr generic_argument ->
+    std_ppcmds
 
 val pr_raw_extend:
   (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->