Adapt to rocq-prover/rocq#21129.

ppedrot · ppedrot · commit 2a3ad399ad00 · 2025-09-28T13:54:30.000+02:00
diff --git a/Construction/Coproduct.v b/Construction/Coproduct.v
@@ -46,7 +46,7 @@ Next Obligation.
   equivalence;
   destruct x, y; simpl; intuition;
   unfold Coproduct_obligation_1 in *;
-  intuition.
+  intuition; auto with *.
 Qed.
 Next Obligation.
   repeat match goal with [ H : _ + _ |- _ ] => destruct H end;
@@ -57,7 +57,7 @@ Next Obligation.
   destruct x, y, z;
   unfold Coproduct_obligation_1 in *;
   unfold Coproduct_obligation_3 in *;
-  intuition.
+  intuition; auto with *.
 Qed.
 Next Obligation.
   destruct x, y;
diff --git a/Construction/Free/Quiver.v b/Construction/Free/Quiver.v
@@ -304,7 +304,7 @@ Proof.
     (Build_QuiverHomomorphism Q1 Q3 (Basics.compose (@fnodes _ _ G) (@fnodes _ _ F)) _ _).
   unshelve eapply Build_SetoidMorphism.
   + exact (fun f => (fedgemap (fedgemap f))).
-  + cat_simpl.
+  + auto with *.
 Defined.
 
 #[export] Instance QuiverHomomorphismEquivalence_IsEquivalence (Q Q': Quiver)
diff --git a/Instance/Cat/Cartesian.v b/Instance/Cat/Cartesian.v
@@ -24,7 +24,7 @@ Program Instance Cat_Cartesian : @Cartesian Cat := {
              ; fmap := fun _ _ => snd |};
 }.
 Next Obligation. proper; apply fmap_respects; auto. Qed.
-Next Obligation. simplify; rewrite !fmap_comp; intuition. Qed.
+Next Obligation. simplify; rewrite !fmap_comp; intuition; auto with *. Qed.
 Next Obligation.
   rename x into A.
   rename y into B.
diff --git a/Instance/Lambda/Multi.v b/Instance/Lambda/Multi.v
@@ -82,7 +82,7 @@ Proof.
   apply value_is_nf in H.
   unfold normal_form in H.
   induction X; auto.
-  now intuition.
+  now intuition; auto with *.
 Qed.
 
 Lemma multistep_AppR {Γ dom cod} {e e' : Γ ⊢ dom} {v : Γ ⊢ (dom ⟶ cod)} :
diff --git a/Instance/Parallel.v b/Instance/Parallel.v
@@ -86,29 +86,29 @@ Program Definition Parallel : Category := {|
 |}.
 Next Obligation. equivalence; reduce. Qed.
 Next Obligation. exact (f; X0). Defined.
-Next Obligation. reduce; intuition. Qed.
+Next Obligation. reduce; intuition; auto with *. Qed.
 Next Obligation. intuition; discriminate. Qed.
 Next Obligation. intuition; discriminate. Qed.
 Next Obligation. intuition; discriminate. Qed.
 Next Obligation.
   proper.
-  destruct x, y, z; simpl in *; intuition.
+  destruct x, y, z; simpl in *; intuition; auto with *.
 Defined.
 Next Obligation.
   destruct x, y; simpl in *;
-  destruct f; intuition.
+  destruct f; intuition; auto with *.
 Qed.
 Next Obligation.
   destruct x, y; simpl in *;
-  destruct f; intuition.
+  destruct f; intuition; auto with *.
 Qed.
 Next Obligation.
   destruct x, y, z, w; simpl in *;
-  destruct f; intuition.
+  destruct f; intuition; auto with *.
 Qed.
 Next Obligation.
   destruct x, y, z, w; simpl in *;
-  destruct f; intuition.
+  destruct f; intuition; auto with *.
 Qed.
 
 Require Import Category.Theory.Functor.
@@ -130,7 +130,7 @@ Program Definition APair {C : Category} {x y : C} (f g : x ~> y) :
     | ParY, ParX => False_rect _ (ParHom_Y_X_absurd _ (projT2 h))
     end
 |}.
-Next Obligation. proper; reduce; simpl; intuition. Qed.
+Next Obligation. proper; reduce; simpl; intuition; auto with *. Qed.
 Next Obligation. destruct x0; simpl; cat. Qed.
 Next Obligation.
   destruct x0, y0, z; simpl; auto with parallel_laws; cat.
diff --git a/Instance/Rel.v b/Instance/Rel.v
@@ -43,14 +43,14 @@ Next Obligation.
   - destruct H as [? [? H2]].
     destruct H2; assumption.
   - exists y0.
-    intuition.
+    intuition; auto with *.
 Qed.
 Next Obligation.
   split; intros.
   - destruct H as [? [H1 ?]].
     destruct H1; assumption.
   - exists x0.
-    intuition.
+    intuition; auto with *.
 Qed.
 Next Obligation. firstorder. Qed.
 Next Obligation. firstorder. Qed.
diff --git a/Instance/Sets/Cartesian/Closed.v b/Instance/Sets/Cartesian/Closed.v
@@ -27,12 +27,12 @@ Program Instance Sets_Closed : @Closed Sets _ := {
 Next Obligation.
   proper; destruct f; simpl.
   apply proper_morphism.
-  split; simpl; intuition.
+  split; simpl; intuition; auto with *.
 Qed.
 Next Obligation.
   proper; destruct f; simpl.
   apply proper_morphism.
-  split; simpl; intuition.
+  split; simpl; intuition; auto with *.
 Qed.
 Next Obligation.
   proper; simpl in *.
diff --git a/Instance/Two.v b/Instance/Two.v
@@ -50,7 +50,7 @@ Program Definition _2 : Category := {|
     | _,    _,    _    => _
     end
 |}.
-Next Obligation. destruct x, y, z; intuition. Qed.
+Next Obligation. destruct x, y, z; intuition; auto with *. Qed.
 Next Obligation.
   destruct x, y, z; auto with two_laws;
   intuition; discriminate.
@@ -65,7 +65,7 @@ Next Obligation.
 Qed.
 Next Obligation. destruct f; auto. Qed.
 Next Obligation. destruct f; auto. Qed.
-Next Obligation. destruct x, y, z, w; auto with two_laws; intuition. Qed.
+Next Obligation. destruct x, y, z, w; auto with two_laws; intuition; auto with *. Qed.
 Next Obligation. destruct x, y, z, w; auto with two_laws; intuition. Qed.
 
 Require Import Category.Instance.Sets.
diff --git a/Instance/Two/Discrete.v b/Instance/Two/Discrete.v
@@ -51,7 +51,7 @@ Program Definition Two_Discrete : Category := {|
     | _,    _,    _    => _
     end
 |}.
-Next Obligation. destruct x, y, z; intuition. Qed.
+Next Obligation. destruct x, y, z; intuition; auto with *. Qed.
 Next Obligation.
   destruct x, y, z; auto with two_laws;
   intuition; discriminate.
diff --git a/Lib/Datatypes.v b/Lib/Datatypes.v
@@ -162,7 +162,7 @@ Program Instance sum_setoid {A B} `{Setoid A} `{Setoid B} :
     end
 }.
 Next Obligation.
-  equivalence; destruct x, y; try destruct z; intuition.
+  equivalence; destruct x, y; try destruct z; intuition; auto with *.
 Qed.
 
 #[global]
diff --git a/Lib/FMapExt.v b/Lib/FMapExt.v
@@ -247,9 +247,9 @@ Proof.
   apply F.Equal_mapsto_iff; split; intros.
     simplify_maps.
       rewrite <- H3.
-      simplify_maps; intuition.
+      simplify_maps; intuition; auto with *.
       simplify_maps.
-    simplify_maps; intuition.
+    simplify_maps; intuition; auto with *.
   simplify_maps.
   simplify_maps.
     rewrite H1.
@@ -277,12 +277,12 @@ Proof.
     simplify_maps.
   simplify_maps.
     simplify_maps.
-    intuition.
+    intuition; auto with *.
     rewrite <- H3.
     assumption.
   simplify_maps.
   simplify_maps.
-  intuition.
+  intuition; auto with *.
 Qed.
 
 Lemma in_mapsto_iff : ∀ elt k (m : M.t elt),
@@ -474,7 +474,7 @@ Proof.
     repeat simplify_maps.
   - apply F.Equal_mapsto_iff; split; intros;
     repeat simplify_maps;
-    right; intuition; simplify_maps.
+    right; intuition; auto with *; simplify_maps.
 Qed.
 
 Lemma add_associative {elt}
@@ -642,7 +642,7 @@ Qed.
 Obligation 2.
   intros x y Heq.
   destruct x, y; simpl in *; trivial.
-  intuition.
+  intuition; auto with *.
 Qed.
 Obligation 3.
   intros x y z Heq1 Heq2.
@@ -661,12 +661,12 @@ Program Instance pairP_Equivalence {A B} (P : relation A) (Q : relation B) :
 Obligation 1.
   intro x.
   destruct x; simpl.
-  intuition.
+  intuition; auto with *.
 Qed.
 Obligation 2.
   intros x y Heq.
   destruct x, y; simpl in *.
-  intuition.
+  intuition; auto with *.
 Qed.
 Obligation 3.
   intros x y z Heq1 Heq2.
diff --git a/Lib/MapDecide.v b/Lib/MapDecide.v
@@ -60,7 +60,7 @@ Local Set Warnings "-intuition-auto-with-star".
 
 Lemma term_beq_sound x y : term_beq x y = true → x = y.
 Proof.
-  induction x, y; simpl; intros; intuition.
+  induction x, y; simpl; intros; intuition; auto with *.
   - apply Pos.eqb_eq in H; subst; reflexivity.
   - apply N.eqb_eq in H; subst; reflexivity.
 Defined.
diff --git a/Lib/Tactics.v b/Lib/Tactics.v
@@ -86,7 +86,7 @@ Ltac cat :=
     [H : equiv ?X ?Y, H' : equiv ?Y ?Z |- equiv ?X ?Z] => transitivity Y
   end : category_laws.
 
-Ltac equivalence := constructor; repeat intro; simpl; try cat; intuition.
+Ltac equivalence := constructor; repeat intro; simpl; try cat; intuition; auto with *.
 Ltac proper := repeat intro; simpl; try cat; intuition.
 Ltac sapply F :=
   let H := fresh "H" in pose proof F as H; cbn in H; apply H; clear H.
diff --git a/Solver/Normal.v b/Solver/Normal.v
@@ -337,7 +337,7 @@ Fixpoint exprAD (e : Expr) : Type :=
 
 Theorem exprAD_sound (e : Expr) : exprAD e ↔ exprD e.
 Proof.
-  induction e; split; simpl in *; intuition.
+  induction e; split; simpl in *; intuition; auto with *.
   - destruct (termD _ _ _) eqn:?; [|tauto].
     destruct (termD _ _ (_ (_ g))) eqn:?; [|tauto].
     apply from_morphism_to_morphism in Heqo.
