Adapt to rocq-prover/rocq#21129.

Author: ppedrot

src/Misc.v

@@ -1654,7 +1654,7 @@ Arguments forallb2 {A B} f l1 l2.
 (* Misc lemmas *)
 
 Lemma neg_eq_true_eq_false b : b = false <-> b <> true.
-Proof. destruct b; intuition. Qed.
+Proof. destruct b; intuition; auto with *. Qed.
 
 Lemma is_true_iff e :  e = true <-> is_true e.
 Proof. now unfold is_true. Qed.

src/QInst.v

@@ -78,7 +78,7 @@ Lemma impl_or_split_right a b c:
   implb (a || b) c = true -> negb b || c = true.
 Proof.
   intro H.
-  destruct a; destruct c; intuition.
+  destruct a; destruct c; intuition; auto with *.
 Qed.
 
 Lemma impl_or_split_left a b c:
@@ -93,7 +93,7 @@ Lemma eqb_sym_or_split_right a b c:
   Bool.eqb c (a || b) = true -> negb b || c = true.
 Proof.
   intro H.
-  destruct a; destruct c; intuition.
+  destruct a; destruct c; intuition; auto with *.
 Qed.
 
 Lemma eqb_sym_or_split_left a b c:
@@ -107,7 +107,7 @@ Lemma eqb_or_split_right a b c:
   Bool.eqb (a || b) c = true -> negb b || c = true.
 Proof.
   intro H.
-  destruct a; destruct c; intuition.
+  destruct a; destruct c; intuition; auto with *.
 Qed.
 
 Lemma eqb_or_split_left a b c:
@@ -131,7 +131,7 @@ Lemma impl_and_split_right a b c:
   implb a (b && c) = true -> negb a || c = true.
 Proof.
   intro H.
-  destruct a; destruct c; intuition.
+  destruct a; destruct c; intuition; auto with *.
 Qed.
 
 Lemma impl_and_split_left a b c:

src/array/FArray.v

@@ -1170,14 +1170,14 @@ Section FArray.
   Proof.
     intros (l,Hl,Hd); induction l as [ |a l IHl].
     - intros (l',Hl',Hd'); unfold eq; simpl.
-      destruct l'; unfold equal; simpl; intuition.
+      destruct l'; unfold equal; simpl; intuition; auto with *.
     - intros (l',Hl',Hd'); unfold eq.
       destruct l' as [ |p l'].
-      + destruct a; unfold equal; simpl; intuition.
+      + destruct a; unfold equal; simpl; intuition; auto with *.
       + destruct a as (x,e).
         destruct p as (x',e').
         unfold equal; simpl.
-        destruct (compare x x') as [Hlt|Heq|Hlt]; simpl; [intuition| |intuition].
+        destruct (compare x x') as [Hlt|Heq|Hlt]; simpl; [intuition; auto with *| |intuition; auto with *].
         split.
         * intros [H0 H1].
           unfold cmp, compare2eqb at 1.

src/lia/Lia.v

@@ -1249,13 +1249,13 @@ Transparent build_z_atom.
       intros p H18; rewrite H5; auto with smtcoq_core; rewrite H10; eauto with smtcoq_core arith.
       split.
       case (Lit.is_pos a); case (Lit.is_pos b); simpl; rewrite H11; rewrite (bounded_bformula_le _ _ H9 _ H6); auto with smtcoq_core.
-      simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto with smtcoq_core; try discriminate; simpl; intuition.
+      simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto with smtcoq_core; try discriminate; simpl; intuition; auto with *.
       (* Fiff *)
       simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split.
       intros p H18; rewrite H5; auto with smtcoq_core; rewrite H10; eauto with smtcoq_core arith.
       split.
       case (Lit.is_pos a); case (Lit.is_pos b); simpl; rewrite H11; rewrite (bounded_bformula_le _ _ H9 _ H6); auto with smtcoq_core.
-      simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto with smtcoq_core; try discriminate; simpl; intuition.
+      simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto with smtcoq_core; try discriminate; simpl; intuition; auto with *.
       (* Fite *)
       simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2; case_eq (build_var vm2 (Lit.blit c)); try discriminate; intros [vm3 f3] Heq3 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; destruct (Hbv _ _ _ _ Heq3 H8) as [H13 [H14 [H15 [H16 H17]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split.
       intros p H18; rewrite H5; auto with smtcoq_core; rewrite H10; eauto with smtcoq_core arith.