Merge PR #13098: Deprecating wit_var to the benefit of its synonymous wit_hyp

Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Reviewed-by: ppedrot

13 files changed, 32 insertions, 38 deletions

diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index f1f538ab39..b7ac71181a 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -20,8 +20,6 @@ open Tacarg
 open Names
 open Logic
 
-let wit_hyp = wit_var
-
 }
 
 DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 863c4d37d8..ad4374dba3 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -47,7 +47,7 @@ let () =
 
 let () =
   let register name entry = Tacentries.register_tactic_notation_entry name entry in
-  register "hyp" wit_var;
+  register "hyp" wit_hyp;
   register "simple_intropattern" wit_simple_intropattern;
   register "integer" wit_integer;
   register "reference" wit_ref;
@@ -140,7 +140,7 @@ ARGUMENT EXTEND occurrences
   GLOB_PRINTED BY { pr_occurrences }
 
 | [ ne_integer_list(l) ] -> { ArgArg l }
-| [ var(id) ] -> { ArgVar id }
+| [ hyp(id) ] -> { ArgVar id }
 END
 
 {
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4f20e5a800..a2a47c0bf4 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -33,8 +33,6 @@ open Proofview.Notations
 open Attributes
 open Vernacextend
 
-let wit_hyp = wit_var
-
 }
 
 DECLARE PLUGIN "ltac_plugin"
@@ -450,7 +448,7 @@ END
 (* Subst                                                              *)
 
 TACTIC EXTEND subst
-| [ "subst" ne_var_list(l) ] -> { subst l }
+| [ "subst" ne_hyp_list(l) ] -> { subst l }
 | [ "subst" ] -> { subst_all () }
 END
 
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 2e72ceae5a..44472a1995 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -18,8 +18,6 @@ open Pcoq.Constr
 open Pltac
 open Hints
 
-let wit_hyp = wit_var
-
 }
 
 DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 8331927cda..ee94fd565a 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -29,8 +29,6 @@ open Pvernac.Vernac_
 open Pltac
 open Vernacextend
 
-let wit_hyp = wit_var
-
 }
 
 DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index cbb53497d3..fe896f9351 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1323,7 +1323,7 @@ let () =
   register_basic_print0 wit_smart_global
     (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global;
   register_basic_print0 wit_ident pr_id pr_id pr_id;
-  register_basic_print0 wit_var pr_lident pr_lident pr_id;
+  register_basic_print0 wit_hyp pr_lident pr_lident pr_id;
   register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"];
   register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env;
   Genprint.register_print0
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index f7037176d2..ee28229cb7 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -161,8 +161,8 @@ let coerce_var_to_ident fresh env sigma v =
     match out_gen (topwit wit_intro_pattern) v with
     | { CAst.v=IntroNaming (IntroIdentifier id)} -> id
     | _ -> fail ()
-  else if has_type v (topwit wit_var) then
-    out_gen (topwit wit_var) v
+  else if has_type v (topwit wit_hyp) then
+    out_gen (topwit wit_hyp) v
   else match Value.to_constr v with
   | None -> fail ()
   | Some c ->
@@ -184,8 +184,8 @@ let id_of_name = function
   | Some (IntroNaming (IntroIdentifier id)) -> id
   | Some _ -> fail ()
   | None ->
-  if has_type v (topwit wit_var) then
-    out_gen (topwit wit_var) v
+  if has_type v (topwit wit_hyp) then
+    out_gen (topwit wit_hyp) v
   else
     match Value.to_constr v with
     | None -> fail ()
@@ -222,8 +222,8 @@ let coerce_to_intro_pattern sigma v =
   match is_intro_pattern v with
   | Some pat -> pat
   | None ->
-  if has_type v (topwit wit_var) then
-    let id = out_gen (topwit wit_var) v in
+  if has_type v (topwit wit_hyp) then
+    let id = out_gen (topwit wit_hyp) v in
     IntroNaming (IntroIdentifier id)
   else match Value.to_constr v with
   | Some c when isVar sigma c ->
@@ -259,8 +259,8 @@ let coerce_to_constr env v =
     ([], c)
   else if has_type v (topwit wit_constr_under_binders) then
     out_gen (topwit wit_constr_under_binders) v
-  else if has_type v (topwit wit_var) then
-    let id = out_gen (topwit wit_var) v in
+  else if has_type v (topwit wit_hyp) then
+    let id = out_gen (topwit wit_hyp) v in
     (try [], constr_of_id env id with Not_found -> fail ())
   else fail ()
 
@@ -282,8 +282,8 @@ let coerce_to_evaluable_ref env sigma v =
   | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> EvalVarRef id
   | Some _ -> fail ()
   | None ->
-  if has_type v (topwit wit_var) then
-    let id = out_gen (topwit wit_var) v in
+  if has_type v (topwit wit_hyp) then
+    let id = out_gen (topwit wit_hyp) v in
     if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
     else fail ()
   else if has_type v (topwit wit_ref) then
@@ -328,8 +328,8 @@ let coerce_to_hyp env sigma v =
   | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> id
   | Some _ -> fail ()
   | None ->
-  if has_type v (topwit wit_var) then
-    let id = out_gen (topwit wit_var) v in
+  if has_type v (topwit wit_hyp) then
+    let id = out_gen (topwit wit_hyp) v in
     if is_variable env id then id else fail ()
   else match Value.to_constr v with
   | Some c when isVar sigma c -> destVar sigma c
@@ -360,8 +360,8 @@ let coerce_to_quantified_hypothesis sigma v =
   | Some (IntroNaming (IntroIdentifier id)) -> NamedHyp id
   | Some _ -> raise (CannotCoerceTo "a quantified hypothesis")
   | None ->
-  if has_type v (topwit wit_var) then
-    let id = out_gen (topwit wit_var) v in
+  if has_type v (topwit wit_hyp) then
+    let id = out_gen (topwit wit_hyp) v in
     NamedHyp id
   else if has_type v (topwit wit_int) then
     AnonHyp (out_gen (topwit wit_int) v)
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index f0ca813b08..d58a76fe13 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -219,7 +219,9 @@ let interp_prod_item = function
     | None ->
       if String.Map.mem s !entry_names then String.Map.find s !entry_names
       else begin match ArgT.name s with
-      | None -> user_err Pp.(str ("Unknown entry "^s^"."))
+      | None ->
+         if s = "var" then user_err Pp.(str ("var is deprecated, use hyp.")) (* to remove in 8.14 *)
+         else user_err Pp.(str ("Unknown entry "^s^"."))
       | Some arg -> arg
       end
     | Some n ->
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index dea216045e..9c3b05fdf1 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -835,7 +835,7 @@ let () =
   Genintern.register_intern0 wit_ref (lift intern_global_reference);
   Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
   Genintern.register_intern0 wit_ident intern_ident';
-  Genintern.register_intern0 wit_var (lift intern_hyp);
+  Genintern.register_intern0 wit_hyp (lift intern_hyp);
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_ltac (lift intern_ltac);
   Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index eaeae50254..12bfb4d09e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -971,8 +971,8 @@ let interp_destruction_arg ist gl arg =
           match v with
           | {v=IntroNaming (IntroIdentifier id)} -> try_cast_id id
           | _ -> error ()
-        else if has_type v (topwit wit_var) then
-          let id = out_gen (topwit wit_var) v in
+        else if has_type v (topwit wit_hyp) then
+          let id = out_gen (topwit wit_hyp) v in
           try_cast_id id
         else if has_type v (topwit wit_int) then
           keep,ElimOnAnonHyp (out_gen (topwit wit_int) v)
@@ -1238,7 +1238,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
   | ArgVar {loc;v=id} ->
       let v =
         try Id.Map.find id ist.lfun
-        with Not_found -> in_gen (topwit wit_var) id
+        with Not_found -> in_gen (topwit wit_hyp) id
       in
       let open Ftactic in
       force_vrec ist v >>= begin fun v ->
@@ -1529,7 +1529,7 @@ and interp_genarg ist x : Val.t Ftactic.t =
     let open Ftactic.Notations in
     (* Ad-hoc handling of some types. *)
     let tag = genarg_tag x in
-    if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then
+    if argument_type_eq tag (unquote (topwit (wit_list wit_hyp))) then
       interp_genarg_var_list ist x
     else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then
       interp_genarg_constr_list ist x
@@ -1573,9 +1573,9 @@ and interp_genarg_var_list ist x =
   Ftactic.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
-  let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in
+  let lc = Genarg.out_gen (glbwit (wit_list wit_hyp)) x in
   let lc = interp_hyp_list ist env sigma lc in
-  let lc = in_list (val_tag wit_var) lc in
+  let lc = in_list (val_tag wit_hyp) lc in
   Ftactic.return lc
   end
 
@@ -2096,7 +2096,7 @@ let () =
   register_interp0 wit_ref (lift interp_reference);
   register_interp0 wit_pre_ident (lift interp_pre_ident);
   register_interp0 wit_ident (lift interp_ident);
-  register_interp0 wit_var (lift interp_hyp);
+  register_interp0 wit_hyp (lift interp_hyp);
   register_interp0 wit_intropattern (lifts interp_intro_pattern) [@warning "-3"];
   register_interp0 wit_simple_intropattern (lifts interp_intro_pattern);
   register_interp0 wit_clause_dft_concl (lift interp_clause);
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index fd869b225f..ec44ae4698 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -282,7 +282,7 @@ let () =
   Genintern.register_subst0 wit_smart_global subst_global_reference;
   Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
   Genintern.register_subst0 wit_ident (fun _ v -> v);
-  Genintern.register_subst0 wit_var (fun _ v -> v);
+  Genintern.register_subst0 wit_hyp (fun _ v -> v);
   Genintern.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"];
   Genintern.register_subst0 wit_simple_intropattern subst_intro_pattern;
   Genintern.register_subst0 wit_tactic subst_tactic;
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d859fe51ab..cb58b9bcb8 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -280,7 +280,7 @@ let interp_wit wit ist gl x =
   sigma, Tacinterp.Value.cast (topwit wit) arg
 
 let interp_hyp ist gl (SsrHyp (loc, id)) =
-  let s, id' = interp_wit wit_var ist gl CAst.(make ?loc id) in
+  let s, id' = interp_wit wit_hyp ist gl CAst.(make ?loc id) in
   if not_section_id id' then s, SsrHyp (loc, id') else
   hyp_err ?loc "Can't clear section hypothesis " id'
 
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 89e0c9fcbe..7b584b5159 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -155,7 +155,7 @@ let pr_ssrhyp _ _ _ = pr_hyp
 let wit_ssrhyprep = add_genarg "ssrhyprep" (fun env sigma -> pr_hyp)
 
 let intern_hyp ist (SsrHyp (loc, id) as hyp) =
-  let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in
+  let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_hyp) CAst.(make ?loc id)) in
   if not_section_id id then hyp else
   hyp_err ?loc "Can't clear section hypothesis " id