Adapt w.r.t. coq/coq#18909.

src/Algebra/Field.v

@@ -20,7 +20,7 @@ Section Field.
 
   Lemma right_multiplicative_inverse : forall x : T, ~ eq x zero -> eq (mul x (inv x)) one.
   Proof using Type*.
-    intros. rewrite commutative. auto using left_multiplicative_inverse.
+    intros. rewrite commutative. pose left_multiplicative_inverse; eauto.
   Qed.
 
   Lemma left_inv_unique x ix : ix * x = one -> ix = inv x.
@@ -79,7 +79,7 @@ Section Field.
 
   Global Instance integral_domain : @integral_domain T eq zero one opp add sub mul.
   Proof using Type*.
-    split; auto using field_commutative_ring, field_is_zero_neq_one, is_mul_nonzero_nonzero.
+    split; eauto using field_commutative_ring, field_is_zero_neq_one, is_mul_nonzero_nonzero.
   Qed.
 End Field.
 
@@ -137,7 +137,7 @@ Section Homomorphism.
     intros.
     eapply inv_unique.
     rewrite <-Ring.homomorphism_mul.
-    rewrite left_multiplicative_inverse; auto using Ring.homomorphism_one.
+    rewrite left_multiplicative_inverse; pose Ring.homomorphism_one; eauto.
   Qed.
 
   Lemma homomorphism_multiplicative_inverse_complete

src/Algebra/Group.v

@@ -10,13 +10,13 @@ Section BasicProperties.
   Local Open Scope eq_scope.
 
   Lemma cancel_left : forall z x y, z*x = z*y <-> x = y.
-  Proof using Type*. eauto using Monoid.cancel_left, left_inverse. Qed.
+  Proof using Type*. epose Monoid.cancel_left; epose left_inverse; eauto. Qed.
   Lemma cancel_right : forall z x y, x*z = y*z <-> x = y.
-  Proof using Type*. eauto using Monoid.cancel_right, right_inverse. Qed.
+  Proof using Type*. epose Monoid.cancel_right; epose right_inverse; eauto. Qed.
   Lemma inv_inv x : inv(inv(x)) = x.
-  Proof using Type*. eauto using Monoid.inv_inv, left_inverse. Qed.
+  Proof using Type*. epose Monoid.inv_inv; epose left_inverse; eauto. Qed.
   Lemma inv_op_ext x y : (inv y*inv x)*(x*y) =id.
-  Proof using Type*. eauto using Monoid.inv_op, left_inverse. Qed.
+  Proof using Type*. epose Monoid.inv_op; epose left_inverse; eauto. Qed.
 
   Lemma inv_unique x ix : ix * x = id -> ix = inv x.
   Proof using Type*.

src/Algebra/Hierarchy.v

@@ -156,7 +156,7 @@ Section ZeroNeqOne.
 
   Lemma one_neq_zero : not (eq one zero).
   Proof using Type*.
-    intro HH; symmetry in HH. auto using zero_neq_one.
+    intro HH; symmetry in HH. epose zero_neq_one; auto.
   Qed.
 End ZeroNeqOne.
 

src/Algebra/IntegralDomain.v

@@ -17,7 +17,7 @@ Module IntegralDomain.
     Global Instance Integral_domain :
       @Integral_domain.Integral_domain T zero one add mul sub opp eq Ring.Ncring_Ring_ops
                                        Ring.Ncring_Ring Ring.Cring_Cring_commutative_ring.
-    Proof using Type. split; cbv; eauto using zero_product_zero_factor, one_neq_zero. Qed.
+    Proof using Type. split; cbv; pose zero_product_zero_factor; pose one_neq_zero; eauto. Qed.
   End IntegralDomain.
 
   Module _LargeCharacteristicReflective.

src/Algebra/Ring.v

@@ -96,7 +96,9 @@ Section Ring.
   Global Instance Ncring_Ring_ops : @Ncring.Ring_ops T zero one add mul sub opp eq := {}.
   Global Instance Ncring_Ring : @Ncring.Ring T zero one add mul sub opp eq Ncring_Ring_ops.
   Proof using Type*.
-    split; exact _ || cbv; intros; eauto using left_identity, right_identity, commutative, associative, right_inverse, left_distributive, right_distributive, ring_sub_definition with core typeclass_instances.
+    split; exact _ || cbv; intros;
+    pose left_identity; pose right_identity; pose commutative; pose associative; pose right_inverse; pose left_distributive; pose right_distributive; pose ring_sub_definition;
+    eauto with core typeclass_instances.
     - (* TODO: why does [eauto using @left_identity with typeclass_instances] not work? *)
       eapply @left_identity; eauto with typeclass_instances.
     - eapply @right_identity; eauto with typeclass_instances.

src/LegacyArithmetic/BarretReduction.v

@@ -33,7 +33,7 @@ Section barrett.
            /\ small_valid barrett_reduce }.
   Proof.
     intro x. evar (pr : SmallT); exists pr. intros x_valid.
-    assert (0 <= decode_large x < b^(k+offset) * b^(k-offset)) by auto using decode_medium_valid.
+    assert (0 <= decode_large x < b^(k+offset) * b^(k-offset)) by eauto using decode_medium_valid.
     assert (0 <= decode_large x < b^(2 * k)) by (autorewrite with pull_Zpow zsimplify in *; lia).
     assert ((decode_large x) mod b^(k-offset) < b^(k-offset)) by auto with zarith lia.
     rewrite (barrett_reduction_small m b (decode_large x) k μ offset) by lia.

src/LegacyArithmetic/MontgomeryReduction.v

@@ -41,10 +41,10 @@ Section montgomery.
            /\ small_valid partial_reduce }.
   Proof.
     intro T. evar (pr : SmallT); exists pr. intros T_valid.
-    assert (0 <= decode_large T < small_bound * small_bound) by auto using decode_large_valid.
-    assert (0 <= decode_small (Mod_SmallBound T) < small_bound) by auto using decode_small_valid, Mod_SmallBound_valid.
-    assert (0 <= decode_small modulus' < small_bound) by auto using decode_small_valid.
-    assert (0 <= decode_small modulus_digits < small_bound) by auto using decode_small_valid, modulus_digits_valid.
+    assert (0 <= decode_large T < small_bound * small_bound) by eauto using decode_large_valid.
+    assert (0 <= decode_small (Mod_SmallBound T) < small_bound) by eauto using decode_small_valid, Mod_SmallBound_valid.
+    assert (0 <= decode_small modulus' < small_bound) by eauto using decode_small_valid.
+    assert (0 <= decode_small modulus_digits < small_bound) by eauto using decode_small_valid, modulus_digits_valid.
     assert (0 <= modulus) by apply (modulus_nonneg _).
     assert (modulus < small_bound) by (rewrite <- modulus_digits_correct; lia).
     rewrite <- partial_reduce_alt_eq by lia.
@@ -61,10 +61,10 @@ Section montgomery.
            /\ small_valid reduce }.
   Proof.
     intro T. evar (pr : SmallT); exists pr. intros T_valid.
-    assert (0 <= decode_large T < small_bound * small_bound) by auto using decode_large_valid.
-    assert (0 <= decode_small (Mod_SmallBound T) < small_bound) by auto using decode_small_valid, Mod_SmallBound_valid.
-    assert (0 <= decode_small modulus' < small_bound) by auto using decode_small_valid.
-    assert (0 <= decode_small modulus_digits < small_bound) by auto using decode_small_valid, modulus_digits_valid.
+    assert (0 <= decode_large T < small_bound * small_bound) by eauto using decode_large_valid.
+    assert (0 <= decode_small (Mod_SmallBound T) < small_bound) by eauto using decode_small_valid, Mod_SmallBound_valid.
+    assert (0 <= decode_small modulus' < small_bound) by eauto using decode_small_valid.
+    assert (0 <= decode_small modulus_digits < small_bound) by eauto using decode_small_valid, modulus_digits_valid.
     assert (0 <= modulus) by apply (modulus_nonneg _).
     assert (modulus < small_bound) by (rewrite <- modulus_digits_correct; lia).
     unfold reduce_via_partial.

src/Spec/CompleteEdwardsCurve.v

@@ -32,7 +32,7 @@ Module E.
       end.
 
     Program Definition zero : point := (0, 1).
-    Next Obligation. eauto using Pre.onCurve_zero. Qed.
+    Next Obligation. pose Pre.onCurve_zero; eauto. Qed.
 
     Program Definition add (P1 P2:point) : point :=
       match coordinates P1, coordinates P2 return (F*F) with

src/Util/Relations.v

@@ -3,7 +3,7 @@ Require Import Crypto.Util.Logic.
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Setoids.Setoid.
 
 Lemma symmetry_iff {T} {R} {Rsym:@Symmetric T R} x y: R x y <-> R y x.
-  intuition eauto using symmetry.
+  epose symmetry; intuition eauto.
 Qed.
 
 Lemma and_rewrite_l {A B} {RA RB} {Equivalence_RA:Equivalence RA} {Equivalence_RB:Equivalence RB}