Merge pull request #675 from PrincetonUniversity/coq8.17deprecations

Fix Coq 8.17 deprecations

compcert/cfrontend/Ctypes.v

@@ -1902,7 +1902,7 @@ Theorem link_match_program_gen:
   exists tp, link tp1 tp2 = Some tp /\ match_program p tp.
 Proof.
   intros until p; intros L [M1 T1] [M2 T2].
-  exploit link_linkorder; eauto. intros [LO1 LO2]. 
+  destruct (link_linkorder _ _ _ L) as [LO1 LO2].
 Local Transparent Linker_program.
   simpl in L; unfold link_program in L.
   destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate.

floyd/VSU.v

@@ -2373,7 +2373,7 @@ revert G G_LNR Gsub; induction builtins as [|[i?]]; [ simpl; induction fs as [|[
   simpl in H5.
   pose proof (eqb_ident_spec i j).
   destruct (eqb_ident i j); inv H5.
-  assert (i <> j) by (clear - H6; intuition). clear H6.
+  assert (i <> j) by (clear - H6; intuition congruence). clear H6.
   apply (in_map fst) in H4. specialize (Gsub _ H4). simpl in Gsub; destruct Gsub; auto.
   contradiction.
   auto.

floyd/field_at.v

@@ -1630,7 +1630,7 @@ Lemma is_pointer_or_null_field_address_lemma:
 Proof.
 intros.
 unfold field_address.
-if_tac; intuition.
+if_tac; intuition (auto; try solve [contradiction]).
 Qed.
 
 Lemma isptr_field_address_lemma:
@@ -1640,7 +1640,7 @@ Lemma isptr_field_address_lemma:
 Proof.
 intros.
 unfold field_address.
-if_tac; intuition.
+if_tac; intuition (auto; try solve [contradiction]).
 Qed.
 
 Lemma eval_lvar_spec: forall id t rho,

floyd/field_compat.v

@@ -354,7 +354,7 @@ Proof.
   rewrite H1.
   simpl. apply andp_derives; auto.
   2: apply derives_refl. 
-  apply prop_derives. intuition.
+  apply prop_derives. intuition auto with field_compatible.
   assert (sublist n1 (Z.min n (Zlength v')) v' = sublist n1 n v').
   f_equal. autorewrite with sublist. auto.
   rewrite H2.
@@ -409,7 +409,7 @@ intros until 1. intros NA ?H ?H Hni Hii Hp. subst p'.
   assert (SS': (sizeof t * n + sizeof t * (n'-n) = sizeof t * n')%Z).
   rewrite <- Z.mul_add_distr_l. f_equal. lia.
   hnf in H|-*.
-  intuition.
+  intuition auto with field_compatible.
   *
   destruct p; try contradiction.
   clear - SP SS SS' H H4 H0 H5 H3 H8 Hni Hii.

floyd/functional_base.v

@@ -359,7 +359,7 @@ Ltac putable' x :=
  | Z.sub ?x ?y => putable x; putable y
  | Z.mul ?x ?y => putable x; putable y
  | Z.div ?x ?y => putable x; putable y
- | Zmod ?x ?y => putable x; putable y
+ | Z.modulo ?x ?y => putable x; putable y
  | Z.max ?x ?y => putable x; putable y
  | Z.opp ?x => putable x
  | Ceq => idtac

msl/age_to.v

@@ -77,7 +77,7 @@ Qed.
 
 Lemma age_to_eq k {A} `{agA : ageable A} (x : A) : k = level x -> age_to k x = x.
 Proof.
-  intros ->; apply age_to_ge, Le.le_refl.
+  intros ->; apply age_to_ge, PeanoNat.Nat.le_refl.
 Qed.
 
 Lemma age_age_to n {A} `{agA : ageable A} x y : level x = S n -> age x y -> age_to n x = y.

msl/eq_dec.v

@@ -55,7 +55,7 @@ Arguments upd_neq [A H B] _ _ _ _ _.
 Proof.
   repeat intro.
  destruct (Compare_dec.lt_eq_lt_dec a a') as [[?|?]| ?]; auto;
-  right; intro; subst; eapply Lt.lt_irrefl; eauto.
+  right; intro; subst; eapply PeanoNat.Nat.lt_irrefl; eauto.
 Defined.
 
 #[global] Instance EqDec_prod (A: Type) (EA: EqDec A) (B: Type) (EB: EqDec B) : EqDec (A*B).

msl/knot_full.v

@@ -528,7 +528,7 @@ Module KnotFull (TF':TY_FUNCTOR_FULL) : KNOT_FULL with Module TF:=TF'.
     simpl.
     unfold knot_level_def; simpl; auto.
     auto.
-    eapply Le.le_trans; eauto.
+    eapply PeanoNat.Nat.le_trans; eauto.
     inv H0.
     unfold knot_level_def; simpl; auto.
 

msl/predicates_hered.v

@@ -344,7 +344,7 @@ Definition necM  : modality
 
 #[local] Hint Resolve rt_refl rt_trans t_trans : core.
 #[local] Hint Unfold necR : core.
-Obligation Tactic := unfold hereditary; intuition;
+Local Obligation Tactic := unfold hereditary; intuition;
     first [eapply pred_hereditary; eauto; fail | eapply pred_upclosed; eauto; fail | eauto ].
 
 (* Definitions of the basic propositional conectives.

msl/predicates_hered_simple.v

@@ -203,7 +203,7 @@ Definition necM {A} `{ageable A} : modality
 
 #[export] Hint Resolve rt_refl rt_trans t_trans : core.
 #[export] Hint Unfold necR : core.
-Obligation Tactic := unfold hereditary; intuition;
+Local Obligation Tactic := unfold hereditary; intuition;
     first [eapply pred_hereditary; eauto; fail | eauto ].
 
 (* Definitions of the basic propositional conectives.

msl/predicates_rec.v

@@ -123,7 +123,7 @@ Proof.
     apply pred_upclosed with x'; auto.
     apply pred_nec_hereditary with a''; auto.
     specialize (H2 _ _ (necR_refl _) (ext_refl _)).
-    apply (@HORec'_unage _ _ _ X f Hcont (n - level a'') (level a'') b a'' (Le.le_refl _)) in H2.
+    apply (@HORec'_unage _ _ _ X f Hcont (n - level a'') (level a'') b a'' (PeanoNat.Nat.le_refl _)) in H2.
     generalize (necR_level _ _ H); intro.
     pose proof (ext_level _ _ H0) as Hl0.
     replace (n - level a'' + level a'') with n in H2 by lia.
@@ -136,7 +136,7 @@ Proof.
     assert (app_pred (HORec' f (level a) x) a).
     rewrite H. apply H2.
      clear - H3 H4 H5 Hcont.
-    apply (@HORec'_unage _ _ _ X f Hcont (level a - level x'') (level x'') x x'' (Le.le_refl _)).
+    apply (@HORec'_unage _ _ _ X f Hcont (level a - level x'') (level x'') x x'' (PeanoNat.Nat.le_refl _)).
     pose proof (ext_level _ _ H4).
     replace (level a - level x'' + level x'') with (level a)
         by (apply necR_level in H3; lia).

msl/predicates_sl.v

@@ -102,7 +102,7 @@ Definition extendM : modality
   := exist _ extendR valid_rel_extend.
 
 (* Definitions of the BI connectives. *)
-Obligation Tactic := unfold hereditary; intros; try solve [intuition].
+Local Obligation Tactic := unfold hereditary; intros; try solve [intuition].
 
 (* This is the key point of the ordered logic: emp is true of anything
    that's in the extension order with an identity.

msl/predicates_sl_simple.v

@@ -79,7 +79,7 @@ Definition extendM {A}{JA: Join A}{PA: Perm_alg A}{SA : Sep_alg A}{AG: ageable A
   := exist _ extendR valid_rel_extend.
 
 (* Definitions of the BI connectives. *)
-Obligation Tactic := unfold hereditary; intros; try solve [intuition].
+Local Obligation Tactic := unfold hereditary; intros; try solve [intuition].
 
 Program Definition emp {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : pred A := identity.
 Next Obligation.

msl/tree_shares.v

@@ -158,24 +158,24 @@ Module Share <: SHARE_MODEL.
 
   Lemma nonEmpty_dec : forall x, {nonEmptyTree x}+{~nonEmptyTree x}.
   Proof.
-    induction x; simpl; intros; invert_ord; destruct_bool; intuition.
+    induction x; simpl; intros; invert_ord; destruct_bool; intuition auto with bool.
   Defined.
 
   Lemma nonFull_dec : forall x, {nonFullTree x}+{~nonFullTree x}.
   Proof.
-    induction x; simpl; intros; invert_ord; destruct_bool; intuition.
+    induction x; simpl; intros; invert_ord; destruct_bool; intuition auto with bool.
   Defined.
 
   Lemma geTrueFull : forall x,
       shareTreeOrd (Leaf true) x -> ~nonFullTree x.
   Proof.
-    induction x; simpl; intros; invert_ord; destruct_bool; intuition.
+    induction x; simpl; intros; invert_ord; destruct_bool; intuition auto with bool.
   Qed.
 
   Lemma leFalseEmpty : forall x,
       shareTreeOrd x (Leaf false) -> ~nonEmptyTree x.
   Proof.
-    induction x; simpl; intros; invert_ord; destruct_bool; intuition.
+    induction x; simpl; intros; invert_ord; destruct_bool; intuition auto with bool.
   Qed.
 
   Lemma emptyLeFalse : forall x,
@@ -208,14 +208,14 @@ Module Share <: SHARE_MODEL.
   Lemma eqFalseLeaf_empty : forall x,
     shareTreeEq (Leaf false) x -> ~nonEmptyTree x.
   Proof.
-    induction x; simpl; intros; invert_ord; destruct_bool; intuition.
+    induction x; simpl; intros; invert_ord; destruct_bool; intuition auto with bool.
   Qed.
 
   Lemma eqTrueLeaf_full : forall x,
     shareTreeEq (Leaf true) x ->
     ~nonFullTree x.
   Proof.
-    induction x; simpl; intros; invert_ord; destruct_bool; intuition.
+    induction x; simpl; intros; invert_ord; destruct_bool; intuition auto with bool.
   Qed.
 
   Lemma emptyTree_canonical_falseLeaf : forall x,
@@ -250,7 +250,7 @@ Module Share <: SHARE_MODEL.
     shareTreeOrd (Leaf b) x3 ->
     shareTreeOrd x1 x3.
   Proof.
-    intro x1; induction x1; simpl; intros; invert_ord; destruct_bool; intuition.
+    intro x1; induction x1; simpl; intros; invert_ord; destruct_bool; intuition auto with bool.
     inv H0; invert_ord; destruct_bool; intuition eauto.
     discriminate.
     inv H0; invert_ord; destruct_bool; intuition eauto.

sepcomp/reach.v

@@ -503,13 +503,13 @@ Proof. intros. unfold sharedSrc. rewrite replace_locals_shared.
 extensionality b. unfold  shared_of, join.
 remember (foreign_of mu b) as d.
 destruct d; simpl; trivial.
-  destruct p. intuition.
+  destruct p. intuition auto with bool.
 remember (pubSrc' b) as q. symmetry in Heqq.
 destruct q; simpl. apply HPUB1 in Heqq.
   destruct (local_of mu b); trivial. congruence.
 unfold pub_of. destruct mu; simpl in *.
 specialize (HPUB2 b).
-destruct (pubBlocksSrc b); trivial. rewrite Heqq in HPUB2. intuition.
+destruct (pubBlocksSrc b); trivial. rewrite Heqq in HPUB2. intuition congruence.
 Qed.
 
 Definition getBlocks (V:list val) (b: block): bool :=
@@ -686,10 +686,10 @@ Proof. intros.
          rewrite getBlocksD_nil in H0.
          rewrite getBlocksD.
          destruct x; try congruence.
-         apply orb_true_iff in H0. destruct H0; intuition.
+         apply orb_true_iff in H0. destruct H0; intuition auto with bool.
    apply IHInj. intros. apply HR.
       rewrite getBlocksD. rewrite H0.
-      destruct x; trivial. intuition.
+      destruct x; trivial. intuition auto with bool.
 Qed.
 
 Lemma restrict_mapped_closed: forall j m X
@@ -805,7 +805,7 @@ Proof. intros. unfold exportedSrc in SRC. unfold exportedTgt.
    exists b2, d. rewrite J, G. intuition.
   destruct (shared_SrcTgt _ WD _ SRC) as [b2 [d [J G]]].
    exists b2, d. rewrite (shared_in_all _ WD _ _ _ J).
-      rewrite G. intuition.
+      rewrite G. intuition auto with bool.
 Qed.
 
 Lemma val_inject_sub_on j k: forall v1 v2
@@ -879,7 +879,7 @@ Proof. intros.
  apply sharedSrc_iff in H. destruct H as [jb [delta SH]].
    specialize (HB _ _ _ SH).
    exists jb, delta.
-   intuition.
+   intuition auto with bool.
 Qed.
 
 Lemma REACH_as_inj: forall mu (WD: SM_wd mu) m1 m2 vals1 vals2
@@ -900,7 +900,7 @@ Proof. intros.
    specialize (HB _ _ _ SH).
    apply shared_in_all in SH; trivial.
    exists jb, delta.
-   intuition.
+   intuition auto with bool.
 Qed.
 
 Lemma REACH_local: forall mu (WD: SM_wd mu) m1 m2 vals1 vals2
@@ -933,7 +933,7 @@ Proof. intros.
   destruct (joinD_Some _ _ _ _ _ ASINJ). assumption.
   destruct H.
   destruct (local_DomRng _ WD _ _ _ H0) as [ZZ _]; rewrite ZZ in locBSrc.
-  intuition.
+  discriminate.
 Qed.
 
 (*The following six or so results are key lemmas about REACH - they say
@@ -1001,7 +1001,7 @@ Proof. intros.
     apply H.
   destruct H as [_ H].
     destruct (local_DomRng _ WD _ _ _ H) as [ZZ _]; rewrite ZZ in locBSrc.
-    intuition.
+    discriminate.
 Qed.
 
 Lemma pubBlocksSrc_REACH: forall m1 mu (WD: SM_wd mu) vals b, pubBlocksSrc mu b = true ->
@@ -1129,7 +1129,7 @@ Proof. intros.
     apply restrictI_Some. assumption.
     apply Glob.
     unfold isGlobalBlock.
-      apply genv2blocksBool_char2 in H. rewrite H. intuition.
+      apply genv2blocksBool_char2 in H. rewrite H. intuition auto with bool.
   destruct (restrictD_Some _ _ _ _ _ H0) as [AU XX]; clear H0.
      apply (PGc _ _ _ H AU).
 Qed.
@@ -1242,8 +1242,8 @@ Proof. intros.
               destruct H0.
                 rewrite (meminj_preserves_globals_isGlobalBlock _ _ PG _ H0).
                 exists b, 0. rewrite <- (genvs_domain_eq_isGlobal _ _ GenvsDomEQ).
-                intuition.
-              destruct (H _ H0) as [b2 [d [J GB2]]]. exists b2, d; intuition.
+                intuition auto with bool.
+              destruct (H _ H0) as [b2 [d [J GB2]]]. exists b2, d; intuition auto with bool.
   split. intros.
          destruct (HR _ H0) as [b2 [d [J R2]]].
          apply (HypJ _ _ _ J).
@@ -1254,7 +1254,7 @@ Proof. intros.
   split. split; intros. apply (HS _ H0). apply (HT _ H0).
   split. eapply meminj_preserves_globals_initSM; intuition.
   split. apply meminj_preserves_globals_init_REACH_frgn; try eassumption.
-    intuition.
+    intuition auto with bool.
   split. simpl. apply REACH_is_closed.
   rewrite initial_SM_as_inj.
     apply (inject_REACH_closed _ _ _ MInj).
@@ -1359,7 +1359,7 @@ intros.
   unfold DomSrc.
   rewrite L', (frgnBlocksSrc_extBlocksSrc _ WDnu' _ F'); simpl.
   apply (frgnSrc_shared _ WDnu') in F'.
-  apply REACH_nil. unfold exportedSrc. intuition.
+  apply REACH_nil. unfold exportedSrc. intuition auto with bool.
 Qed.
 
 Lemma restrict_SharedSrc mu: SM_wd mu ->
@@ -1458,7 +1458,7 @@ Lemma restrict_sm_local': forall mu (WD: SM_wd mu) X
 Proof. intros. rewrite restrict_sm_local.
  apply restrict_outside. intros.
  apply HX.
- destruct (local_DomRng _ WD _ _ _ H). unfold vis. intuition.
+ destruct (local_DomRng _ WD _ _ _ H). unfold vis. intuition auto with bool.
 Qed.
 
 Lemma restrict_sm_pub': forall mu (WD: SM_wd mu) X
@@ -1468,7 +1468,7 @@ Lemma restrict_sm_pub': forall mu (WD: SM_wd mu) X
 Proof. intros. rewrite restrict_sm_pub.
  apply restrict_outside. intros.
  apply HX. apply pub_in_local in H.
- destruct (local_DomRng _ WD _ _ _ H). unfold vis. intuition.
+ destruct (local_DomRng _ WD _ _ _ H). unfold vis. intuition auto with bool.
 Qed.
 
 Lemma restrict_sm_foreign': forall mu (WD: SM_wd mu) X
@@ -1559,7 +1559,7 @@ split; intros.
     rewrite restrict_sm_frgnBlocksTgt, restrict_sm_extern.
     exists b2, d1. split; trivial.
     apply restrictI_Some; intuition.
-    apply HX. unfold vis. rewrite H. intuition.
+    apply HX. unfold vis. rewrite H. intuition auto with bool.
   rewrite restrict_sm_locBlocksTgt.
     rewrite restrict_sm_pubBlocksTgt in H.
     apply (pubBlocksLocalTgt _ WD _ H).
@@ -1735,7 +1735,7 @@ Proof. intros.
                        eapply REACH_cons; try eassumption.
                        destruct (joinD_Some _ _ _ _ _ IHL); clear IHL.
                          apply REACH_nil. unfold exportedSrc, sharedSrc, shared_of, join.
-                           rewrite H5.  intuition.
+                           rewrite H5.  intuition auto with bool.
                          destruct H5.
                            remember (locBlocksSrc mu b' && REACH m1 (exportedSrc mu vals1) b') as qq.
                            destruct qq; inv H6. apply eq_sym in Heqqq. apply andb_true_iff in Heqqq. apply Heqqq.
@@ -1792,7 +1792,7 @@ Lemma local_of_vis mu: forall b1 b2 d
    (WD: SM_wd mu), vis mu b1 = true.
 Proof. intros. unfold vis.
   destruct (local_DomRng _ WD _ _ _ LOC).
-  intuition.
+  intuition auto with bool.
 Qed.
 
 Lemma incr_local_restrictvis mu: SM_wd mu ->
@@ -1801,13 +1801,13 @@ Proof. intros; red; intros.
   apply restrictI_Some.
   apply local_in_all; assumption.
   destruct (local_DomRng _ H _ _ _ H0) .
-  unfold vis; intuition.
+  unfold vis; intuition auto with bool.
 Qed.
 
 Lemma local_visTgt mu (WD: SM_wd mu) b1 b2 d:
       local_of mu b1 = Some(b2,d) -> visTgt mu b2 = true.
 Proof. unfold visTgt. intros.
-  destruct (local_DomRng _ WD _ _ _ H); intuition.
+  destruct (local_DomRng _ WD _ _ _ H); intuition auto with bool.
 Qed.
 
 Section globalfunction_ptr_inject.
@@ -1837,7 +1837,7 @@ Lemma restrict_GFP_vis: forall mu
 Proof. intros.
   unfold vis.
   eapply restrict_preserves_globalfun_ptr. eassumption.
-  intuition.
+  intuition auto with bool.
 Qed.
 
 Remark val_inject_function_pointer: