Added Genarg as generic argument type.

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

9 files changed, 20 insertions, 1 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6184501550..4857b16cc1 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -362,6 +362,7 @@ let rec pr_argument_type = function
   | VarArgType -> str"var"
   | RefArgType -> str"ref"
   (* Specific types *)
+  | GenArgType -> str"genarg"
   | SortArgType -> str"sort"
   | ConstrArgType -> str"constr"
   | ConstrMayEvalArgType -> str"constr-may-eval"
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index e3ee3db404..71ba6b0215 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -37,6 +37,7 @@ let rec make_wit loc = function
   | VarArgType -> <:expr< Genarg.wit_var >>
   | RefArgType -> <:expr< Genarg.wit_ref >>
   | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >>
+  | GenArgType -> <:expr< Genarg.wit_genarg >>
   | SortArgType -> <:expr< Genarg.wit_sort >>
   | ConstrArgType -> <:expr< Genarg.wit_constr >>
   | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 6aefd3b720..0f5be6efb7 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -215,6 +215,7 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
   | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
   | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
+  | Genarg.GenArgType -> <:expr< Genarg.GenArgType >>
   | Genarg.SortArgType -> <:expr< Genarg.SortArgType >>
   | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
   | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >>
diff --git a/interp/genarg.ml b/interp/genarg.ml
index f9b5bee0a4..ea8302e91c 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -24,6 +24,7 @@ type argument_type =
   | VarArgType
   | RefArgType
   (* Specific types *)
+  | GenArgType
   | SortArgType
   | ConstrArgType
   | ConstrMayEvalArgType
@@ -48,6 +49,7 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2
 | VarArgType, VarArgType -> true
 | RefArgType, RefArgType -> true
+| GenArgType, GenArgType -> true
 | SortArgType, SortArgType -> true
 | ConstrArgType, ConstrArgType -> true
 | ConstrMayEvalArgType, ConstrMayEvalArgType -> true
@@ -118,6 +120,8 @@ let wit_ref = RefArgType
 
 let wit_quant_hyp = QuantHypArgType
 
+let wit_genarg = GenArgType
+
 let wit_sort = SortArgType
 
 let wit_constr = ConstrArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 4f5dea7ec0..8f4b816187 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -214,6 +214,7 @@ type argument_type =
   | VarArgType
   | RefArgType
   (** Specific types *)
+  | GenArgType
   | SortArgType
   | ConstrArgType
   | ConstrMayEvalArgType
@@ -262,6 +263,8 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen
 
 val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
 
+val wit_genarg : (raw_generic_argument, glob_generic_argument, typed_generic_argument) genarg_type
+
 val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
 
 val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 35e153e0fb..350d96142d 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -150,6 +150,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen (rawwit wit_ident) x)
   | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
   | RefArgType -> prref (out_gen (rawwit wit_ref) x)
+  | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
   | SortArgType -> pr_glob_sort (out_gen (rawwit wit_sort) x)
   | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
   | ConstrMayEvalArgType ->
@@ -193,6 +194,7 @@ let rec pr_glob_generic prc prlc prtac prpat x =
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen (glbwit wit_ident) x)
   | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
   | RefArgType -> pr_or_var (pr_located pr_global) (out_gen (glbwit wit_ref) x)
+  | GenArgType -> pr_glob_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
   | SortArgType -> pr_glob_sort (out_gen (glbwit wit_sort) x)
   | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
   | ConstrMayEvalArgType ->
@@ -237,6 +239,7 @@ let rec pr_generic prc prlc prtac prpat x =
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen (topwit wit_ident) x)
   | VarArgType -> pr_id (out_gen (topwit wit_var) x)
   | RefArgType -> pr_global (out_gen (topwit wit_ref) x)
+  | GenArgType -> pr_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
   | SortArgType -> pr_sort (out_gen (topwit wit_sort) x)
   | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
   | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index aa91db9b0e..883b9094f2 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -787,6 +787,8 @@ and intern_genarg ist x =
       in_gen (glbwit wit_var) (intern_hyp ist (out_gen (rawwit wit_var) x))
   | RefArgType ->
       in_gen (glbwit wit_ref) (intern_global_reference ist (out_gen (rawwit wit_ref) x))
+  | GenArgType ->
+      in_gen (glbwit wit_genarg) (intern_genarg ist (out_gen (rawwit wit_genarg) x))
   | SortArgType ->
       in_gen (glbwit wit_sort) (out_gen (rawwit wit_sort) x)
   | ConstrArgType ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 82354c815e..4847362d3a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1561,6 +1561,8 @@ and interp_genarg ist gl x =
       in_gen (topwit wit_var) (interp_hyp ist gl (out_gen (glbwit wit_var) x))
     | RefArgType ->
       in_gen (topwit wit_ref) (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x))
+    | GenArgType ->
+      in_gen (topwit wit_genarg) (interp_genarg ist gl (out_gen (glbwit wit_genarg) x))
     | SortArgType ->
       let (sigma,c_interp) =
 	pf_interp_constr ist gl
@@ -2057,7 +2059,7 @@ and interp_atomic ist gl tac =
       tac args ist
   | TacAlias (loc,s,l,(_,body)) -> fun gl ->
     let evdref = ref gl.sigma in
-    let f x = match genarg_tag x with
+    let rec f x = match genarg_tag x with
     | IntArgType ->
         of_tacvalue (VInteger (out_gen (glbwit wit_int) x))
     | IntOrVarArgType ->
@@ -2075,6 +2077,7 @@ and interp_atomic ist gl tac =
     | RefArgType ->
         of_tacvalue (VConstr ([],constr_of_global
           (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x))))
+    | GenArgType -> f (out_gen (glbwit wit_genarg) x)
     | SortArgType ->
         of_tacvalue (VConstr ([],mkSort (interp_sort (out_gen (glbwit wit_sort) x))))
     | ConstrArgType ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index bb7caf93b4..3070cf01cc 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -313,6 +313,7 @@ and subst_genarg subst (x:glob_generic_argument) =
   | RefArgType ->
       in_gen (glbwit wit_ref) (subst_global_reference subst
 	(out_gen (glbwit wit_ref) x))
+  | GenArgType -> in_gen (glbwit wit_genarg) (subst_genarg subst (out_gen (glbwit wit_genarg) x))
   | SortArgType ->
       in_gen (glbwit wit_sort) (out_gen (glbwit wit_sort) x)
   | ConstrArgType ->