Adapt w.r.t. coq/coq#18895. (#1866)

src/AbstractInterpretation/Proofs.v

@@ -149,7 +149,10 @@ Module Compilers.
       Local Notation bottom_Proper := (@bottom_Proper base_type abstract_domain' bottom' abstract_domain'_R bottom'_Proper).
       Local Notation bottom_for_each_lhs_of_arrow_Proper := (@bottom_for_each_lhs_of_arrow_Proper base_type abstract_domain' bottom' abstract_domain'_R bottom'_Proper).
 
-      Local Hint Resolve (@bottom_Proper) (@bottom_for_each_lhs_of_arrow_Proper) : core typeclass_instances.
+      Local Hint Extern 0 (Proper _) => simple apply (@bottom_Proper) : typeclass_instances.
+      Local Hint Extern 0 (Proper _) => simple apply (@bottom_for_each_lhs_of_arrow_Proper) : typeclass_instances.
+      Local Hint Extern 0 => simple apply (@bottom_Proper) : core.
+      Local Hint Extern 0 => simple apply (@bottom_for_each_lhs_of_arrow_Proper) : core.
 
       Fixpoint related_bounded_value {t} : abstract_domain t -> value t -> type.interp base_interp t -> Prop
         := match t return abstract_domain t -> value t -> type.interp base_interp t -> Prop with

src/Util/Equality.v

@@ -121,7 +121,7 @@ Section hprop.
 
   Let hprop_encode {x y : A} (p : x = y) : unit := tt.
 
-  Local Hint Resolve (fun x => @isiso_encode A x (fun _ => unit)) : typeclass_instances.
+  Local Hint Extern 1 => simple apply (fun x => @isiso_encode A x (fun _ => unit)) : typeclass_instances.
 
   Global Instance ishprop_path_hprop : IsHPropRel (@eq A).
   Proof.

src/Util/ZUtil/Div.v

@@ -377,8 +377,9 @@ Module Z.
   Qed.
 
 #[global]
-  Hint Resolve (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1))
-       (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith.
+  Hint Extern 2 => simple apply (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith.
+#[global]
+  Hint Extern 2 => simple apply (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith.
 
   Lemma sub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a <? b then -1 else 0.
   Proof.

src/Util/ZUtil/Hints/ZArith.v

@@ -2,7 +2,8 @@ Require Import Coq.ZArith.ZArith.
 Require Export Crypto.Util.ZUtil.Hints.Core.
 
 Global Hint Resolve Z.log2_nonneg Z.log2_up_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r Z.pow_lt_mono_r Z.pow_lt_mono_l Z.pow_lt_mono Z.mul_lt_mono_nonneg Z.div_lt_upper_bound Z.div_pos Zmult_lt_compat_r Z.pow_le_mono_r Z.pow_le_mono_l Z.div_lt Z.div_le_compat_l Z.div_le_mono Z.max_le_compat Z.min_le_compat Z.log2_up_le_mono Z.pow_nonneg : zarith.
-Global Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) : zarith.
+Global Hint Extern 1 => simple apply (fun a b H => proj1 (Z.mod_pos_bound a b H)) : zarith.
+Global Hint Extern 1 => simple apply (fun a b H => proj2 (Z.mod_pos_bound a b H)) : zarith.
 Global Hint Resolve -> Z.pow_gt_1 Z.opp_le_mono Z.pred_le_mono : zarith.
 Global Hint Resolve <- Z.lor_nonneg : zarith.
 

src/Util/ZUtil/LandLorBounds.v

@@ -231,12 +231,20 @@ Module Z.
     apply Z.land_upper_bound_l; rewrite ?Z.land_nonneg; t.
   Qed.
 #[global]
-  Hint Resolve land_round_bound_pos_r (fun v x => proj1 (land_round_bound_pos_r v x)) (fun v x => proj2 (land_round_bound_pos_r v x)) : zarith.
+  Hint Resolve land_round_bound_pos_r : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj1 (land_round_bound_pos_r v x)) : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj2 (land_round_bound_pos_r v x)) : zarith.
   Lemma land_round_bound_pos_l v x
     : 0 <= Z.land (Z.pos x) v <= Z.land (Z.round_lor_land_bound (Z.pos x)) v.
   Proof. rewrite <- !(Z.land_comm v); apply land_round_bound_pos_r. Qed.
 #[global]
-  Hint Resolve land_round_bound_pos_l (fun v x => proj1 (land_round_bound_pos_l v x)) (fun v x => proj2 (land_round_bound_pos_l v x)) : zarith.
+  Hint Resolve land_round_bound_pos_l : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj1 (land_round_bound_pos_l v x)) : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj2 (land_round_bound_pos_l v x)) : zarith.
 
   Lemma land_round_bound_neg_r v x
     : Z.land v (Z.round_lor_land_bound (Z.neg x)) <= Z.land v (Z.neg x) <= v.
@@ -249,12 +257,20 @@ Module Z.
     etransitivity; [ apply Z.land_le; cbn; lia | ]; lia.
   Qed.
 #[global]
-  Hint Resolve land_round_bound_neg_r (fun v x => proj1 (land_round_bound_neg_r v x)) (fun v x => proj2 (land_round_bound_neg_r v x)) : zarith.
+  Hint Resolve land_round_bound_neg_r : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj1 (land_round_bound_neg_r v x)) : zarith.
+#[global]
+  Hint Extern 0 =>  simple apply (fun v x => proj2 (land_round_bound_neg_r v x)) : zarith.
   Lemma land_round_bound_neg_l v x
     : Z.land (Z.round_lor_land_bound (Z.neg x)) v <= Z.land (Z.neg x) v <= v.
   Proof. rewrite <- !(Z.land_comm v); apply land_round_bound_neg_r. Qed.
 #[global]
-  Hint Resolve land_round_bound_neg_l (fun v x => proj1 (land_round_bound_neg_l v x)) (fun v x => proj2 (land_round_bound_neg_l v x)) : zarith.
+  Hint Resolve land_round_bound_neg_l : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj1 (land_round_bound_neg_l v x)) : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj2 (land_round_bound_neg_l v x)) : zarith.
 
   Lemma lor_round_bound_neg_r v x
     : Z.lor v (Z.round_lor_land_bound (Z.neg x)) <= Z.lor v (Z.neg x) <= -1.
@@ -269,12 +285,20 @@ Module Z.
     apply Z.land_upper_bound_l; rewrite ?Z.land_nonneg; t.
   Qed.
 #[global]
-  Hint Resolve lor_round_bound_neg_r (fun v x => proj1 (lor_round_bound_neg_r v x)) (fun v x => proj2 (lor_round_bound_neg_r v x)) : zarith.
+  Hint Resolve lor_round_bound_neg_r : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj1 (lor_round_bound_neg_r v x)) : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj2 (lor_round_bound_neg_r v x)) : zarith.
   Lemma lor_round_bound_neg_l v x
     : Z.lor (Z.round_lor_land_bound (Z.neg x)) v <= Z.lor (Z.neg x) v <= -1.
   Proof. rewrite <- !(Z.lor_comm v); apply lor_round_bound_neg_r. Qed.
 #[global]
-  Hint Resolve lor_round_bound_neg_l (fun v x => proj1 (lor_round_bound_neg_l v x)) (fun v x => proj2 (lor_round_bound_neg_l v x)) : zarith.
+  Hint Resolve lor_round_bound_neg_l : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj1 (lor_round_bound_neg_l v x)) : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj2 (lor_round_bound_neg_l v x)) : zarith.
 
   Lemma lor_round_bound_pos_r v x
     : v <= Z.lor v (Z.pos x) <= Z.lor v (Z.round_lor_land_bound (Z.pos x)).
@@ -287,12 +311,20 @@ Module Z.
     etransitivity; [ | apply Z.lor_lower; rewrite ?Z.lor_nonneg; cbn; lia ]; lia.
   Qed.
 #[global]
-  Hint Resolve lor_round_bound_pos_r (fun v x => proj1 (lor_round_bound_pos_r v x)) (fun v x => proj2 (lor_round_bound_pos_r v x)) : zarith.
+  Hint Resolve lor_round_bound_pos_r : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj1 (lor_round_bound_pos_r v x)) : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj2 (lor_round_bound_pos_r v x)) : zarith.
   Lemma lor_round_bound_pos_l v x
     : v <= Z.lor (Z.pos x) v <= Z.lor (Z.round_lor_land_bound (Z.pos x)) v.
   Proof. rewrite <- !(Z.lor_comm v); apply lor_round_bound_pos_r. Qed.
 #[global]
-  Hint Resolve lor_round_bound_pos_l (fun v x => proj1 (lor_round_bound_pos_l v x)) (fun v x => proj2 (lor_round_bound_pos_l v x)) : zarith.
+  Hint Resolve lor_round_bound_pos_l : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj1 (lor_round_bound_pos_l v x)) : zarith.
+#[global]
+  Hint Extern 0 => simple apply (fun v x => proj2 (lor_round_bound_pos_l v x)) : zarith.
 
   Lemma land_round_bound_pos_r' v x : Z.land v (Z.pos x) <= Z.land v (Z.round_lor_land_bound (Z.pos x)). Proof. auto with zarith. Qed.
   Lemma land_round_bound_pos_l' v x : Z.land (Z.pos x) v <= Z.land (Z.round_lor_land_bound (Z.pos x)) v. Proof. auto with zarith. Qed.

src/Util/ZUtil/Pow.v

@@ -19,11 +19,15 @@ Module Z.
     lia.
   Qed.
 #[global]
-  Hint Resolve nonneg_pow_pos (fun n => nonneg_pow_pos 2 n Z.lt_0_2) : zarith.
+  Hint Resolve nonneg_pow_pos : zarith.
+#[global]
+  Hint Extern 1 => simple apply (fun n => nonneg_pow_pos 2 n Z.lt_0_2) : zarith.
   Lemma nonneg_pow_pos_helper a b dummy : 0 < a -> 0 <= dummy < a^b -> 0 <= b.
   Proof. eauto with zarith lia. Qed.
 #[global]
-  Hint Resolve nonneg_pow_pos_helper (fun n dummy => nonneg_pow_pos_helper 2 n dummy Z.lt_0_2) : zarith.
+  Hint Resolve nonneg_pow_pos_helper : zarith.
+#[global]
+  Hint Extern 2 => simple apply (fun n dummy => nonneg_pow_pos_helper 2 n dummy Z.lt_0_2) : zarith.
 
   Lemma div_pow2succ : forall n x, (0 <= x) ->
     n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x).