Removing ad-hoc interpretation rules for tactic notations and their genarg.

Now that types can share the same dynamic representation, we do not have
to transtype the topelvel values dynamically and just take advantage of
the standard interpretation function.

10 files changed, 25 insertions, 61 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 842f59809..b9336ce33 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -30,11 +30,9 @@ let mk_extraarg loc s =
     <:expr< $lid:"wit_"^s$ >>
 
 let rec make_wit loc = function
-  | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >>
   | IdentArgType -> <:expr< Constrarg.wit_ident >>
   | VarArgType -> <:expr< Constrarg.wit_var >>
   | ConstrArgType -> <:expr< Constrarg.wit_constr >>
-  | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >>
   | OpenConstrArgType -> <:expr< Constrarg.wit_open_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 3088e0365..7001f5f62 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -223,12 +223,10 @@ let mlexpr_of_red_expr = function
       <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
 
 let rec mlexpr_of_argtype loc = function
-  | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
   | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
   | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
   | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
-  | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >>
   | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
   | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
   | Genarg.PairArgType (t1,t2) ->
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 84b056ab6..ab54b6197 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -22,7 +22,8 @@ let loc_of_or_by_notation f = function
 let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type =
   Obj.magic t
 
-let wit_int_or_var = unsafe_of_type IntOrVarArgType
+let wit_int_or_var =
+  Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) None "int_or_var"
 
 let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
   Genarg.make0 None "intropattern"
@@ -43,7 +44,8 @@ let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
 
 let wit_constr = unsafe_of_type ConstrArgType
 
-let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType
+let wit_constr_may_eval =
+  Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval"
 
 let wit_uconstr = Genarg.make0 None "uconstr"
 
@@ -64,11 +66,13 @@ let wit_clause_dft_concl  =
 (** Register location *)
 
 let () =
+  register_name0 wit_int_or_var "Constrarg.wit_int_or_var";
   register_name0 wit_ref "Constrarg.wit_ref";
   register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
   register_name0 wit_tactic "Constrarg.wit_tactic";
   register_name0 wit_sort "Constrarg.wit_sort";
   register_name0 wit_uconstr "Constrarg.wit_uconstr";
+  register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval";
   register_name0 wit_red_expr "Constrarg.wit_red_expr";
   register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl";
   register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp";
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 5cfe3854a..e155a5217 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -15,9 +15,7 @@ let wit_bool : bool uniform_genarg_type =
   make0 None "bool"
 
 let wit_int : int uniform_genarg_type =
-  make0 ~dyn:(val_tag (Obj.magic IntOrVarArgType)) None "int"
-(** FIXME: IntOrVarArgType is hardwired, but that definition should be the other
-    way around. *)
+  make0 None "int"
 
 let wit_string : string uniform_genarg_type =
   make0 None "string"
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 3989cf6df..11a042117 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -13,12 +13,10 @@ module Val = Dyn.Make(struct end)
 
 type argument_type =
   (* Basic types *)
-  | IntOrVarArgType
   | IdentArgType
   | VarArgType
   (* Specific types *)
   | ConstrArgType
-  | ConstrMayEvalArgType
   | OpenConstrArgType
   | ListArgType of argument_type
   | OptArgType of argument_type
@@ -26,11 +24,9 @@ type argument_type =
   | ExtraArgType of string
 
 let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
-| IntOrVarArgType, IntOrVarArgType -> true
 | IdentArgType, IdentArgType -> true
 | VarArgType, VarArgType -> true
 | ConstrArgType, ConstrArgType -> true
-| ConstrMayEvalArgType, ConstrMayEvalArgType -> true
 | OpenConstrArgType, OpenConstrArgType -> true
 | ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2
 | OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2
@@ -40,11 +36,9 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | _ -> false
 
 let rec pr_argument_type = function
-| IntOrVarArgType -> str "int_or_var"
 | IdentArgType -> str "ident"
 | VarArgType -> str "var"
 | ConstrArgType -> str "constr"
-| ConstrMayEvalArgType -> str "constr_may_eval"
 | OpenConstrArgType -> str "open_constr"
 | ListArgType t -> pr_argument_type t ++ spc () ++ str "list"
 | OptArgType t -> pr_argument_type t ++ spc () ++ str "opt"
@@ -168,7 +162,6 @@ let default_empty_value t =
   | None -> None
 
 (** Beware: keep in sync with the corresponding types *)
-let int_or_var_T = Val.create "int"
 let ident_T = Val.create "ident"
 let genarg_T = Val.create "genarg"
 let constr_T = Val.create "constr"
@@ -179,13 +172,10 @@ let list_val = Val.create "list"
 let pair_val = Val.create "pair"
 
 let val_tag = function
-| IntOrVarArgType -> cast_tag int_or_var_T
 | 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
-| ConstrMayEvalArgType -> cast_tag constr_T
-  (** Must ensure that toplevel types of Constr and ConstrMayEval agree! *)
 | OpenConstrArgType -> cast_tag open_constr_T
 | ExtraArgType s -> Obj.magic (String.Map.find s !arg0_map).dyn
 (** Recursive types have no associated dynamic tag *)
@@ -207,9 +197,9 @@ 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
+| IdentArgType
 | VarArgType
-| ConstrArgType | ConstrMayEvalArgType
+| ConstrArgType
 | OpenConstrArgType | ExtraArgType _ -> try_prj wit v
 | ListArgType t ->
   let v = match prj list_val v with
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 89ea49ddb..83ba1dd04 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -201,12 +201,10 @@ val pair_val : (Val.t * Val.t) Val.tag
 
 type argument_type =
   (** Basic types *)
-  | IntOrVarArgType
   | IdentArgType
   | VarArgType
   (** Specific types *)
   | ConstrArgType
-  | ConstrMayEvalArgType
   | OpenConstrArgType
   | ListArgType of argument_type
   | OptArgType of argument_type
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 94cbc54e9..9c6da350f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -267,13 +267,9 @@ 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
-      | 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)
       | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
-      | ConstrMayEvalArgType ->
-        pr_may_eval prc prlc (pr_or_by_notation prref) prpat
-          (out_gen (rawwit wit_constr_may_eval) x)
       | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
       | ListArgType _ ->
         let list_unpacker wit l =
@@ -302,14 +298,9 @@ module Make
 
   let rec pr_glb_generic_rec prc prlc prtac prpat x =
     match Genarg.genarg_tag x with
-      | 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)
       | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
-      | ConstrMayEvalArgType ->
-        pr_may_eval prc prlc
-          (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat
-          (out_gen (glbwit wit_constr_may_eval) x)
       | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
       | ListArgType _ ->
         let list_unpacker wit l =
@@ -337,11 +328,9 @@ module Make
 
   let rec pr_top_generic_rec prc prlc prtac prpat x =
     match Genarg.genarg_tag x with
-      | IntOrVarArgType -> 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)
       | 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))
       | ListArgType _ ->
         let list_unpacker wit l =
@@ -1432,6 +1421,8 @@ let () =
   let pr_bool b = if b then str "true" else str "false" in
   let pr_unit _ = str "()" in
   let pr_string s = str "\"" ++ str s ++ str "\"" in
+  Genprint.register_print0 Constrarg.wit_int_or_var
+    (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
@@ -1462,6 +1453,11 @@ let () =
     (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
     (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
     (fun { Evd.it = it } -> pr_bindings_no_with pr_constr pr_lconstr it);
+  Genprint.register_print0 Constrarg.wit_constr_may_eval
+    (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr)
+    (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)
+      (pr_or_var (pr_and_short_name pr_evaluable_reference)) (pr_pat_and_constr_expr pr_glob_constr))
+    pr_constr;
   Genprint.register_print0 Constrarg.wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index d0f83836d..5e725e182 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -727,7 +727,6 @@ and intern_match_rule onlytac ist = function
 
 and intern_genarg ist x =
   match genarg_tag x with
-  | IntOrVarArgType -> map_raw wit_int_or_var intern_int_or_var ist x
   | IdentArgType ->
     let lf = ref Id.Set.empty in
     map_raw wit_ident (intern_ident lf) ist x
@@ -735,8 +734,6 @@ and intern_genarg ist x =
     map_raw wit_var intern_hyp ist x
   | ConstrArgType ->
     map_raw wit_constr intern_constr ist x
-  | ConstrMayEvalArgType ->
-    map_raw wit_constr_may_eval intern_constr_may_eval ist x
   | OpenConstrArgType ->
     map_raw wit_open_constr (fun ist -> on_snd (intern_constr ist)) ist x
   | ListArgType _ ->
@@ -836,6 +833,7 @@ let () =
   Genintern.register_intern0 wit_clause_dft_concl intern_clause
 
 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_tactic (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_sort (fun ist s -> (ist, s));
@@ -844,6 +842,7 @@ let () =
   Genintern.register_intern0 wit_red_expr (lift intern_red_expr);
   Genintern.register_intern0 wit_bindings (lift intern_bindings);
   Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings);
+  Genintern.register_intern0 wit_constr_may_eval (lift intern_constr_may_eval);
   ()
 
 (***************************************************************************)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5a6834ab5..37d9f1825 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1259,8 +1259,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
           let sigma = Tacmach.New.project gl in
           let env = Proofview.Goal.env gl in
           match tag with
-          | IntOrVarArgType ->
-              Ftactic.return (mk_int_or_var_value ist (Genarg.out_gen (glbwit wit_int_or_var) x))
           | IdentArgType ->
               Ftactic.return (value_of_ident (interp_ident ist env sigma
                                                (Genarg.out_gen (glbwit wit_ident) x)))
@@ -1270,20 +1268,10 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
               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
               Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v)
-          | ConstrMayEvalArgType ->
-              let (sigma,c_interp) =
-                interp_constr_may_eval ist env sigma
-                  (Genarg.out_gen (glbwit wit_constr_may_eval) x)
-              in
-              Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp))
           | ListArgType VarArgType ->
               let wit = glbwit (wit_list wit_var) in
               let ans = List.map (mk_hyp_value ist env sigma) (Genarg.out_gen wit x) in
               Ftactic.return (Value.of_list ans)
-          | ListArgType IntOrVarArgType ->
-              let wit = glbwit (wit_list wit_int_or_var) in
-              let ans = List.map (mk_int_or_var_value ist) (Genarg.out_gen wit x) in
-              Ftactic.return (Value.of_list ans)
           | ListArgType IdentArgType ->
               let wit = glbwit (wit_list wit_ident) in
               let mk_ident x = value_of_ident (interp_ident ist env sigma x) in
@@ -1638,9 +1626,6 @@ and interp_genarg ist env sigma concl gl x =
   let evdref = ref sigma in
   let rec interp_genarg x =
     match genarg_tag x with
-    | IntOrVarArgType ->
-      in_gen (topwit wit_int_or_var)
-        (interp_int_or_var ist (Genarg.out_gen (glbwit wit_int_or_var) x))
     | IdentArgType ->
       in_gen (topwit wit_ident)
         (interp_ident ist env sigma (Genarg.out_gen (glbwit wit_ident) x))
@@ -1652,10 +1637,6 @@ and interp_genarg ist env sigma concl gl x =
       in
       evdref := sigma;
       in_gen (topwit wit_constr) c_interp
-    | ConstrMayEvalArgType ->
-      let (sigma,c_interp) = interp_constr_may_eval ist env !evdref (Genarg.out_gen (glbwit wit_constr_may_eval) x) in
-      evdref := sigma;
-      in_gen (topwit wit_constr_may_eval) c_interp
     | OpenConstrArgType ->
       let expected_type = WithoutTypeConstraint in
       in_gen (topwit wit_open_constr)
@@ -1703,7 +1684,7 @@ and interp_genarg ist env sigma concl gl x =
 
 and global_genarg =
   let rec global_tag = function
-    | IntOrVarArgType -> true
+    | ExtraArgType "int_or_var" -> true (** FIXME *)
     | ListArgType t | OptArgType t -> global_tag t
     | PairArgType (t1,t2) -> global_tag t1 && global_tag t2
     | _ -> false
@@ -2335,6 +2316,7 @@ let interp_constr_with_bindings' ist gl c =
   (project gl, pack_sigma (sigma, c))
 
 let () =
+  Geninterp.register_interp0 wit_int_or_var (fun ist gl n -> project gl, interp_int_or_var ist n);
   Geninterp.register_interp0 wit_ref (lift interp_reference);
   Geninterp.register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
   Geninterp.register_interp0 wit_clause_dft_concl (lift interp_clause);
@@ -2343,7 +2325,9 @@ let () =
   Geninterp.register_interp0 wit_red_expr (lifts interp_red_expr);
   Geninterp.register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis);
   Geninterp.register_interp0 wit_bindings interp_bindings';
-  Geninterp.register_interp0 wit_constr_with_bindings interp_constr_with_bindings'
+  Geninterp.register_interp0 wit_constr_with_bindings interp_constr_with_bindings';
+  Geninterp.register_interp0 wit_constr_may_eval (lifts interp_constr_may_eval);
+  ()
 
 let () =
   let interp ist gl tac =
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 2884e318b..0c9665362 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -280,14 +280,11 @@ and subst_match_rule subst = function
 
 and subst_genarg subst (x:glob_generic_argument) =
   match genarg_tag x with
-  | IntOrVarArgType -> in_gen (glbwit wit_int_or_var) (out_gen (glbwit wit_int_or_var) x)
   | 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))
-  | ConstrMayEvalArgType ->
-      in_gen (glbwit wit_constr_may_eval) (subst_raw_may_eval subst (out_gen (glbwit wit_constr_may_eval) x))
   | OpenConstrArgType ->
       in_gen (glbwit wit_open_constr)
         ((),subst_glob_constr subst (snd (out_gen (glbwit wit_open_constr) x)))
@@ -322,6 +319,7 @@ and subst_genarg subst (x:glob_generic_argument) =
 (** Registering *)
 
 let () =
+  Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
   Genintern.register_subst0 wit_ref subst_global_reference;
   Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
   Genintern.register_subst0 wit_tactic subst_tactic;
@@ -332,4 +330,5 @@ let () =
   Genintern.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis;
   Genintern.register_subst0 wit_bindings subst_bindings;
   Genintern.register_subst0 wit_constr_with_bindings subst_glob_with_bindings;
+  Genintern.register_subst0 wit_constr_may_eval subst_raw_may_eval;
   ()