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

dev/doc/changes.md

@@ -1,27 +1,35 @@
 ## Changes between Coq 8.12 and Coq 8.13
 
-- Tactic language: TacGeneric now takes an argument to tell if it
-  comes from a notation. Use `None` if not and `Some foo` to tell to
-  print such TacGeneric surrounded with `foo:( )`.
-
 ### Code formatting
 
 - The automatic code formatting tool `ocamlformat` has been disabled and its
   git hook removed. If desired, automatic formatting can be achieved by calling
   the `fmt` target of the dune build system.
 
-### Pp library
+### ML API
+
+Abstract syntax of tactic:
+
+- TacGeneric now takes an argument to tell if it comes from a
+  notation. Use `None` if not and `Some foo` to tell to print such
+  TacGeneric surrounded with `foo:( )`.
+
+Printing functions:
 
 - `Pp.h` does not take a `int` argument anymore (the argument was
   not used). In general, where `h n` for `n` non zero was used, `hv n`
   was instead intended. If cancelling the breaking role of cuts in the
   box was intended, turn `h n c` into `h c`.
 
-### Grammar entries
+Grammar entries:
 
 - `Prim.pattern_identref` is deprecated, use `Prim.pattern_ident`
   which now returns a located identifier.
 
+Generic arguments:
+
+- Generic arguments: `wit_var` is deprecated, use `wit_hyp`.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting

interp/stdarg.ml

@@ -40,8 +40,10 @@ let wit_int_or_var =
 let wit_ident =
   make0 "ident"
 
-let wit_var =
-  make0 ~dyn:(val_tag (topwit wit_ident)) "var"
+let wit_hyp =
+  make0 ~dyn:(val_tag (topwit wit_ident)) "hyp"
+
+let wit_var = wit_hyp
 
 let wit_ref = make0 "ref"
 

interp/stdarg.mli

@@ -37,7 +37,10 @@ val wit_int_or_var : (int or_var, int or_var, int) genarg_type
 
 val wit_ident : Id.t uniform_genarg_type
 
+val wit_hyp : (lident, lident, Id.t) genarg_type
+
 val wit_var : (lident, lident, Id.t) genarg_type
+[@@ocaml.deprecated "Use Stdarg.wit_hyp"]
 
 val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
 

parsing/g_prim.mlg

@@ -45,7 +45,7 @@ let test_minus_nat =
 
 GRAMMAR EXTEND Gram
   GLOBAL:
-    bignat bigint natural integer identref name ident var preident
+    bignat bigint natural integer identref name ident hyp preident
     fullyqualid qualid reference dirpath ne_lstring
     ne_string string lstring pattern_ident by_notation
     smart_global bar_cbrace strategy_level;
@@ -58,12 +58,12 @@ GRAMMAR EXTEND Gram
   pattern_ident:
     [ [ LEFTQMARK; id = ident -> { CAst.make ~loc id } ] ]
   ;
-  var: (* as identref, but interpret as a term identifier in ltac *)
-    [ [ id = ident -> { CAst.make ~loc id } ] ]
-  ;
   identref:
     [ [ id = ident -> { CAst.make ~loc id } ] ]
   ;
+  hyp: (* as identref, but interpreted as an hypothesis in tactic notations *)
+    [ [ id = identref -> { id } ] ]
+  ;
   field:
     [ [ s = FIELD -> { Id.of_string s } ] ]
   ;

parsing/pcoq.ml

@@ -279,7 +279,8 @@ module Prim =
     let strategy_level = Entry.create "strategy_level"
 
     (* parsed like ident but interpreted as a term *)
-    let var = Entry.create "var"
+    let hyp = Entry.create "hyp"
+    let var = hyp
 
     let name = Entry.create "name"
     let identref = Entry.create "identref"
@@ -504,7 +505,7 @@ let () =
   Grammar.register0 wit_string (Prim.string);
   Grammar.register0 wit_pre_ident (Prim.preident);
   Grammar.register0 wit_ident (Prim.ident);
-  Grammar.register0 wit_var (Prim.var);
+  Grammar.register0 wit_hyp (Prim.hyp);
   Grammar.register0 wit_ref (Prim.reference);
   Grammar.register0 wit_smart_global (Prim.smart_global);
   Grammar.register0 wit_sort_family (Constr.sort_family);

parsing/pcoq.mli

@@ -173,7 +173,8 @@ module Prim :
     val dirpath : DirPath.t Entry.t
     val ne_string : string Entry.t
     val ne_lstring : lstring Entry.t
-    val var : lident Entry.t
+    val hyp : lident Entry.t
+    val var : lident Entry.t [@@ocaml.deprecated "Use Prim.hyp"]
     val bar_cbrace : unit Entry.t
     val strategy_level : Conv_oracle.level Entry.t
   end

plugins/ltac/coretactics.mlg

@@ -20,8 +20,6 @@ open Tacarg
 open Names
 open Logic
 
-let wit_hyp = wit_var
-
 }
 
 DECLARE PLUGIN "ltac_plugin"

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
 
 {

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
 

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"

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"

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

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)

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 ->

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);

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);

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;

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'
 

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