Adapt w.r.t. coq/coq#18909. (#1881)

Author: ppedrot

src/Algebra/Field.v

@@ -13,7 +13,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.
@@ -72,7 +72,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.
 
@@ -90,7 +90,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

@@ -155,6 +155,6 @@ 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

@@ -16,7 +16,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

@@ -19,7 +19,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/Bedrock/End2End/RupicolaCrypto/ChaCha20.v

@@ -168,7 +168,7 @@ Lemma array_dexpr_locals_put
     map.get l x = None → Forall2 (DEXPR m l) exp w → Forall2 (DEXPR m #{ … l; x => v }#) exp w.
 Proof.
   induction 2; constructor;
-    eauto using dexpr_locals_put.
+    solve [eauto|epose dexpr_locals_put; eauto].
 Qed.
 
 (* we leave prior valiues abstract to support compound operations *)

src/Bedrock/Field/Synthesis/New/Signature.v

@@ -172,7 +172,7 @@ Section WithParameters.
     | |- map word.unsigned ?x = map byte.unsigned _ =>
       is_evar x;
       erewrite Util.map_unsigned_of_Z,MaxBounds.map_word_wrap_bounded
-        by eauto using byte_unsigned_within_max_bounds;
+        by (eapply byte_unsigned_within_max_bounds; eauto);
       reflexivity
     | _ => equivalence_side_conditions_hook
     end.

src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v

@@ -53,7 +53,7 @@ Section OnlyDiffer.
   Proof.
     cbv [equivalent_base rep.equiv rep.Z WeakestPrecondition.dexpr].
     repeat intro; sepsimpl; subst; eexists; sepsimpl; eauto.
-    eauto using expr_only_differ_undef.
+    pose expr_only_differ_undef; eauto.
   Qed.
 
   Section Local.

src/Bedrock/Field/Translation/Proofs/Func.v

@@ -442,7 +442,7 @@ Section Func.
         pose proof H; apply map.only_differ_putmany in H
       end.
 
-      erewrite IHt1; eauto using only_differ_trans; [ |
+      erewrite IHt1; pose only_differ_trans; eauto ; [ |
         apply disjoint_union_l_iff; intuition trivial;
         symmetry; eapply NoDup_disjoint; eauto ].
       erewrite IHt2 by eauto using only_differ_trans.

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