Removing ident and var generic arguments.

9 files changed, 26 insertions, 42 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 639097afa8..9abe5d7cfc 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -30,8 +30,6 @@ let mk_extraarg loc s =
     <:expr< $lid:"wit_"^s$ >>
 
 let rec make_wit loc = function
-  | IdentArgType -> <:expr< Constrarg.wit_ident >>
-  | VarArgType -> <:expr< Constrarg.wit_var >>
   | ConstrArgType -> <:expr< Constrarg.wit_constr >>
   | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
   | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 494ec6ba29..798d428e98 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -223,8 +223,6 @@ let mlexpr_of_red_expr = function
       <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
 
 let rec mlexpr_of_argtype loc = function
-  | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
-  | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
   | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
   | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
   | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 44623f9c9a..94c13fe796 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -31,9 +31,11 @@ let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob
 let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type =
   Genarg.make0 None "tactic"
 
-let wit_ident = unsafe_of_type IdentArgType
+let wit_ident =
+  Genarg.make0 None "ident"
 
-let wit_var = unsafe_of_type VarArgType
+let wit_var =
+  Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) None "var"
 
 let wit_ref = Genarg.make0 None "ref"
 
@@ -68,6 +70,8 @@ let wit_clause_dft_concl  =
 let () =
   register_name0 wit_int_or_var "Constrarg.wit_int_or_var";
   register_name0 wit_ref "Constrarg.wit_ref";
+  register_name0 wit_ident "Constrarg.wit_ident";
+  register_name0 wit_var "Constrarg.wit_var";
   register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
   register_name0 wit_tactic "Constrarg.wit_tactic";
   register_name0 wit_sort "Constrarg.wit_sort";
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 6108c15555..af9ea70ec5 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -56,9 +56,6 @@ struct
 end
 
 type argument_type =
-  (* Basic types *)
-  | IdentArgType
-  | VarArgType
   (* Specific types *)
   | ConstrArgType
   | ListArgType of argument_type
@@ -67,8 +64,6 @@ type argument_type =
   | ExtraArgType of string
 
 let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
-| IdentArgType, IdentArgType -> true
-| VarArgType, VarArgType -> true
 | ConstrArgType, ConstrArgType -> true
 | ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2
 | OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2
@@ -78,8 +73,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | _ -> false
 
 let rec pr_argument_type = function
-| IdentArgType -> str "ident"
-| VarArgType -> str "var"
 | ConstrArgType -> str "constr"
 | ListArgType t -> pr_argument_type t ++ spc () ++ str "list"
 | OptArgType t -> pr_argument_type t ++ spc () ++ str "opt"
@@ -204,13 +197,10 @@ let default_empty_value t =
 
 (** Beware: keep in sync with the corresponding types *)
 let base_create n = Val.Base (Dyn.create n)
-let ident_T = base_create "ident"
 let genarg_T = base_create "genarg"
 let constr_T = base_create "constr"
 
 let rec val_tag = function
-| IdentArgType -> cast_tag ident_T
-| VarArgType -> cast_tag ident_T
   (** Must ensure that toplevel types of Var and Ident agree! *)
 | ConstrArgType -> cast_tag constr_T
 | ExtraArgType s -> cast_tag (String.Map.find s !arg0_map).dyn
@@ -232,8 +222,6 @@ 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
-| IdentArgType
-| VarArgType
 | ConstrArgType
 | ExtraArgType _ -> try_prj wit v
 | ListArgType t ->
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 674ee97ae8..8d929f9f69 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -212,10 +212,8 @@ val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a
 
 type argument_type =
   (** Basic types *)
-  | IdentArgType
-  | VarArgType
-  (** Specific types *)
   | ConstrArgType
+  (** Specific types *)
   | ListArgType of argument_type
   | OptArgType of argument_type
   | PairArgType of argument_type * argument_type
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index a5716279f3..df5f57dac1 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -267,8 +267,6 @@ module Make
 
   let rec pr_raw_generic_rec prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
     match Genarg.genarg_tag x with
-      | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
-      | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
       | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
       | ListArgType _ ->
         let list_unpacker wit l =
@@ -297,8 +295,6 @@ module Make
 
   let rec pr_glb_generic_rec prc prlc prtac prpat x =
     match Genarg.genarg_tag x with
-      | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
-      | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
       | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
       | ListArgType _ ->
         let list_unpacker wit l =
@@ -326,8 +322,6 @@ module Make
 
   let rec pr_top_generic_rec prc prlc prtac prpat x =
     match Genarg.genarg_tag x with
-      | IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
-      | VarArgType -> pr_id (out_gen (topwit wit_var) x)
       | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
       | ListArgType _ ->
         let list_unpacker wit l =
@@ -1415,6 +1409,10 @@ let () =
     (pr_or_var int) (pr_or_var int) int;
   Genprint.register_print0 Constrarg.wit_ref
     pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+  Genprint.register_print0 Constrarg.wit_ident
+    pr_id pr_id pr_id;
+  Genprint.register_print0 Constrarg.wit_var
+    (pr_located pr_id) (pr_located pr_id) pr_id;
   Genprint.register_print0
     Constrarg.wit_intro_pattern
     (Miscprint.pr_intro_pattern pr_constr_expr)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index e6273401dd..ac0c4b266b 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -720,11 +720,6 @@ and intern_match_rule onlytac ist = function
 
 and intern_genarg ist x =
   match genarg_tag x with
-  | IdentArgType ->
-    let lf = ref Id.Set.empty in
-    map_raw wit_ident (intern_ident lf) ist x
-  | VarArgType ->
-    map_raw wit_var intern_hyp ist x
   | ConstrArgType ->
     map_raw wit_constr intern_constr ist x
   | ListArgType _ ->
@@ -823,9 +818,15 @@ let () =
   in
   Genintern.register_intern0 wit_clause_dft_concl intern_clause
 
+let intern_ident' ist id =
+  let lf = ref Id.Set.empty in
+  (ist, intern_ident lf ist id)
+
 let () =
   Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var);
   Genintern.register_intern0 wit_ref (lift intern_global_reference);
+  Genintern.register_intern0 wit_ident intern_ident';
+  Genintern.register_intern0 wit_var (lift intern_hyp);
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_sort (fun ist s -> (ist, s));
   Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5f5adaafb5..adca226303 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1518,11 +1518,11 @@ and interp_match_goal ist lz lr lmr =
 (* Interprets extended tactic generic arguments *)
 and interp_genarg ist x : Val.t Ftactic.t =
     let open Ftactic.Notations in
-    match genarg_tag x with
-    | IdentArgType ->
-      interp_focussed wit_ident (interp_ident ist) x
-    | VarArgType ->
-      interp_focussed wit_var (interp_hyp ist) x
+    (** Ad-hoc handling of some types. *)
+    let tag = genarg_tag x in
+    if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then
+      interp_genarg_var_list ist x
+    else match tag with
     | ConstrArgType ->
       Ftactic.nf_s_enter { s_enter = begin fun gl ->
         let c = Genarg.out_gen (glbwit wit_constr) x in
@@ -1534,8 +1534,6 @@ and interp_genarg ist x : Val.t Ftactic.t =
       end }
     | ListArgType ConstrArgType ->
       interp_genarg_constr_list ist x
-    | ListArgType VarArgType ->
-      interp_genarg_var_list ist x
     | ListArgType _ ->
       let list_unpacker wit l =
         let map x =
@@ -2182,6 +2180,8 @@ let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigm
 let () =
   Geninterp.register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
   Geninterp.register_interp0 wit_ref (lift interp_reference);
+  Geninterp.register_interp0 wit_ident (lift interp_ident);
+  Geninterp.register_interp0 wit_var (lift interp_hyp);
   Geninterp.register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
   Geninterp.register_interp0 wit_clause_dft_concl (lift interp_clause);
   Geninterp.register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s));
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 754c886205..0061237bf3 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -276,9 +276,6 @@ and subst_match_rule subst = function
 
 and subst_genarg subst (x:glob_generic_argument) =
   match genarg_tag x with
-  | IdentArgType ->
-      in_gen (glbwit wit_ident) (out_gen (glbwit wit_ident) x)
-  | VarArgType -> in_gen (glbwit wit_var) (out_gen (glbwit wit_var) x)
   | ConstrArgType ->
       in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x))
   | ListArgType _ ->
@@ -314,6 +311,8 @@ and subst_genarg subst (x:glob_generic_argument) =
 let () =
   Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
   Genintern.register_subst0 wit_ref subst_global_reference;
+  Genintern.register_subst0 wit_ident (fun _ v -> v);
+  Genintern.register_subst0 wit_var (fun _ v -> v);
   Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
   Genintern.register_subst0 wit_tactic subst_tactic;
   Genintern.register_subst0 wit_sort (fun _ v -> v);