Removing the now useless genarg generic argument.

11 files changed, 3 insertions, 26 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index fff7068571..842f59809f 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -33,7 +33,6 @@ let rec make_wit loc = function
   | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >>
   | IdentArgType -> <:expr< Constrarg.wit_ident >>
   | VarArgType -> <:expr< Constrarg.wit_var >>
-  | GenArgType -> <:expr< Constrarg.wit_genarg >>
   | ConstrArgType -> <:expr< Constrarg.wit_constr >>
   | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >>
   | OpenConstrArgType -> <:expr< Constrarg.wit_open_constr >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index be438b54a5..3088e03654 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -227,7 +227,6 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
   | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
-  | Genarg.GenArgType -> <:expr< Genarg.GenArgType >>
   | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
   | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >>
   | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index a67143b005..84b056ab68 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -38,8 +38,6 @@ let wit_ref = Genarg.make0 None "ref"
 
 let wit_quant_hyp = Genarg.make0 None "quant_hyp"
 
-let wit_genarg = unsafe_of_type GenArgType
-
 let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
   Genarg.make0 None "sort"
 
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index fdeddd66a1..ef1ef4aee4 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -38,8 +38,6 @@ 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/lib/genarg.ml b/lib/genarg.ml
index a43a798c46..bf223f99e0 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -17,7 +17,6 @@ type argument_type =
   | IdentArgType
   | VarArgType
   (* Specific types *)
-  | GenArgType
   | ConstrArgType
   | ConstrMayEvalArgType
   | OpenConstrArgType
@@ -30,7 +29,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | IntOrVarArgType, IntOrVarArgType -> true
 | IdentArgType, IdentArgType -> true
 | VarArgType, VarArgType -> true
-| GenArgType, GenArgType -> true
 | ConstrArgType, ConstrArgType -> true
 | ConstrMayEvalArgType, ConstrMayEvalArgType -> true
 | OpenConstrArgType, OpenConstrArgType -> true
@@ -45,7 +43,6 @@ let rec pr_argument_type = function
 | IntOrVarArgType -> str "int_or_var"
 | IdentArgType -> str "ident"
 | VarArgType -> str "var"
-| GenArgType -> str "genarg"
 | ConstrArgType -> str "constr"
 | ConstrMayEvalArgType -> str "constr_may_eval"
 | OpenConstrArgType -> str "open_constr"
@@ -187,7 +184,6 @@ let val_tag = function
 | IntOrVarArgType -> cast_tag int_or_var_T
 | IdentArgType -> cast_tag ident_T
 | VarArgType -> cast_tag var_T
-| GenArgType -> cast_tag genarg_T
 | ConstrArgType -> cast_tag constr_T
 | ConstrMayEvalArgType -> cast_tag constr_may_eval_T
 | OpenConstrArgType -> cast_tag open_constr_T
@@ -212,7 +208,7 @@ let try_prj wit v = match prj (val_tag wit) v with
 let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a =
 fun wit v -> match unquote wit with
 | IntOrVarArgType | IdentArgType
-| VarArgType | GenArgType
+| VarArgType
 | ConstrArgType | ConstrMayEvalArgType
 | OpenConstrArgType | ExtraArgType _ -> try_prj wit v
 | ListArgType t ->
diff --git a/lib/genarg.mli b/lib/genarg.mli
index c431aa619d..89ea49ddb5 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -205,7 +205,6 @@ type argument_type =
   | IdentArgType
   | VarArgType
   (** Specific types *)
-  | GenArgType
   | ConstrArgType
   | ConstrMayEvalArgType
   | OpenConstrArgType
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 4d14cae7a7..b511300758 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -270,7 +270,6 @@ module Make
       | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
       | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
       | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
-      | GenArgType -> pr_raw_generic_rec prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
       | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
       | ConstrMayEvalArgType ->
         pr_may_eval prc prlc (pr_or_by_notation prref) prpat
@@ -306,7 +305,6 @@ module Make
       | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
       | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
       | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
-      | GenArgType -> pr_glb_generic_rec prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
       | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
       | ConstrMayEvalArgType ->
         pr_may_eval prc prlc
@@ -342,7 +340,6 @@ module Make
       | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
       | IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
       | VarArgType -> pr_id (out_gen (topwit wit_var) x)
-      | GenArgType -> pr_top_generic_rec prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
       | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
       | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
       | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index f856fd842b..88e36be14a 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -44,10 +44,7 @@ struct
 
 type t = Val.t
 
-let rec normalize v = v (** FIXME *)
-(*   if has_type v (topwit wit_genarg) then *)
-(*     normalize (out_gen (topwit wit_genarg) v) *)
-(*   else v *)
+let normalize v = v
 
 let of_constr c = in_gen (topwit wit_constr) c
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index ac1229f2f7..d0f83836de 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -733,8 +733,6 @@ and intern_genarg ist x =
     map_raw wit_ident (intern_ident lf) ist x
   | VarArgType ->
     map_raw wit_var intern_hyp ist x
-  | GenArgType ->
-    map_raw wit_genarg intern_genarg ist x
   | ConstrArgType ->
     map_raw wit_constr intern_constr ist x
   | ConstrMayEvalArgType ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1760341d11..f87dc663bc 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1266,7 +1266,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
                                                (Genarg.out_gen (glbwit wit_ident) x)))
           | VarArgType ->
               Ftactic.return (mk_hyp_value ist env sigma (Genarg.out_gen (glbwit wit_var) x))
-          | GenArgType -> f (Genarg.out_gen (glbwit wit_genarg) x)
           | OpenConstrArgType ->
               let (sigma,v) =
                 Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (Genarg.out_gen (glbwit wit_open_constr) x))) gl in
@@ -1647,8 +1646,6 @@ and interp_genarg ist env sigma concl gl x =
         (interp_ident ist env sigma (Genarg.out_gen (glbwit wit_ident) x))
     | VarArgType ->
       in_gen (topwit wit_var) (interp_hyp ist env sigma (Genarg.out_gen (glbwit wit_var) x))
-    | GenArgType ->
-      interp_genarg (Genarg.out_gen (glbwit wit_genarg) x)
     | ConstrArgType ->
       let (sigma,c_interp) =
         interp_constr ist env !evdref (Genarg.out_gen (glbwit wit_constr) x)
@@ -1706,7 +1703,7 @@ and interp_genarg ist env sigma concl gl x =
 
 and global_genarg =
   let rec global_tag = function
-    | IntOrVarArgType | GenArgType -> true
+    | IntOrVarArgType -> true
     | ListArgType t | OptArgType t -> global_tag t
     | PairArgType (t1,t2) -> global_tag t1 && global_tag t2
     | _ -> false
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 6d32aa81b9..2884e318b8 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -284,7 +284,6 @@ and subst_genarg subst (x:glob_generic_argument) =
   | IdentArgType ->
       in_gen (glbwit wit_ident) (out_gen (glbwit wit_ident) x)
   | VarArgType -> in_gen (glbwit wit_var) (out_gen (glbwit wit_var) x)
-  | GenArgType -> in_gen (glbwit wit_genarg) (subst_genarg subst (out_gen (glbwit wit_genarg) x))
   | ConstrArgType ->
       in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x))
   | ConstrMayEvalArgType ->