Merge PR #19006: Deprecate non-reference hints in using clauses of au…

…to-like tactics.

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

doc/changelog/04-tactics/19006-hint-using-deprecate-constr.rst

@@ -0,0 +1,4 @@
+- **Deprecated:**
+  non-reference hints in `using` clauses of :tacn:`auto`-like tactics
+  (`#19006 <https://github.com/coq/coq/pull/19006>`_,
+  by Pierre-Marie Pédrot).

tactics/hints.ml

@@ -1556,6 +1556,10 @@ let hint_globref gr = IsGlobRef gr
 
 let hint_constr (c, diff) = IsConstr (c, diff)
 
+let warn_non_reference_hint_using =
+  CWarnings.create ~name:"non-reference-hint-using" ~category:CWarnings.CoreCategories.deprecated
+    Pp.(fun (env, sigma, c) -> str "Use of the non-reference term " ++ pr_leconstr_env env sigma c ++ str " in \"using\" clauses is deprecated")
+
 let expand_constructor_hints env sigma lems =
   List.map_append (fun lem ->
     let evd, lem = lem env sigma in
@@ -1568,6 +1572,7 @@ let expand_constructor_hints env sigma lems =
     | Var id -> [IsGlobRef (GlobRef.VarRef id)]
     | Construct (cstr, _) -> [IsGlobRef (GlobRef.ConstructRef cstr)]
     | _ ->
+      let () = warn_non_reference_hint_using (env, evd, lem) in
       let (c, ctx) = prepare_hint env sigma (evd,lem) in
       let ctx = if UnivGen.is_empty_sort_context ctx then None else Some ctx in
       [IsConstr (c, ctx)]) lems

test-suite/bugs/bug_4450.v

@@ -18,7 +18,8 @@ Admitted.
 Polymorphic Axiom funi@{i} : f unit@{i}.
 
 Goal (forall U, f U) -> (*(f unit -> False) ->  *)False /\ False.
-  eauto using (fapp unit funi). (* The two fapp's have different universes *)
+  pose (H := fapp unit funi).
+  eauto using H. (* The two fapp's have different universes *)
 Qed.
 
 Definition fapp0 := fapp unit funi.
@@ -51,7 +52,7 @@ Polymorphic Axiom foop@{i} : forall (A : Type@{i}), list A.
 Universe x y.
 Goal list Type@{x}.
 Proof.
-  eauto using (foo Type). (* Refreshes the term *)
+  pose (H := foo Type); eauto using H. (* Refreshes the term *)
   Undo.
   eauto using foo. Show Universes.
   Undo.

test-suite/success/auto.v

@@ -21,9 +21,10 @@ Qed.
 (* Test implicit arguments in "using" clause *)
 
 Goal forall n:nat, nat * nat.
-auto using (pair O).
+epose (H := pair O).
+auto using H.
 Undo.
-eauto using (pair O).
+eauto using H.
 Qed.
 
 Create HintDb test discriminated.

theories/Logic/ChoiceFacts.v

@@ -938,9 +938,8 @@ Corollary fun_reification_descr_computational_excluded_middle_in_prop_context :
   (forall P:Prop, P \/ ~ P) ->
   forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.
 Proof.
-  intros FunReify EM C H. intuition auto using
-    constructive_definite_descr_excluded_middle,
-    (relative_non_contradiction_of_definite_descr (C:=C)).
+  intros FunReify EM C H. pose proof relative_non_contradiction_of_definite_descr (C:=C); intuition auto using
+    constructive_definite_descr_excluded_middle.
 Qed.
 
 (**********************************************************************)

theories/Sorting/PermutSetoid.v

@@ -236,7 +236,8 @@ Lemma permut_remove_hd :
   forall l l1 l2 a,
     permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
 Proof.
-  eauto using permut_remove_hd_eq, (Equivalence_Reflexive (R := eqA)).
+  pose proof (Equivalence_Reflexive (R := eqA));
+  eauto using permut_remove_hd_eq.
 Qed.
 
 Fact if_eqA_else : forall a a' (B:Type)(b b':B),
@@ -499,7 +500,9 @@ Proof.
   - apply permut_cons; auto using Equivalence_Reflexive.
   - change (x :: y :: l) with ([x] ++ y :: l);
       apply permut_add_cons_inside; simpl;
-      apply permut_cons_eq; auto using (Equivalence_Reflexive (R := eqA)), permut_refl.
+      apply permut_cons_eq;
+      pose proof (Equivalence_Reflexive (R := eqA));
+      auto using permut_refl.
   - apply permut_trans with l'; trivial.
 Qed.
 

theories/Structures/OrdersTac.v

@@ -104,7 +104,7 @@ Lemma trans o o' x y z : #o x y -> #o' y z -> #(o+o') x z.
 Proof.
 destruct o, o'; simpl;
 rewrite ?P.le_lteq; intuition auto;
-subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
+subst_eqns; pose proof (StrictOrder_Transitive x y z); eauto with *.
 Qed.
 
 Definition eq_trans x y z : x==y -> y==z -> x==z := @trans OEQ OEQ x y z.