diff --git a/implementations/field_of_fractions.v b/implementations/field_of_fractions.v
index 5470eb5..5eb4d4f 100644
--- a/implementations/field_of_fractions.v
+++ b/implementations/field_of_fractions.v
@@ -116,7 +116,7 @@ Proof.
     rewrite 2!mult_1_r.
     apply (is_ne_0 1).
    unfold dec_recip, Frac_dec_recip.
-   case (decide_rel); simpl; intuition.
+   case (decide_rel); simpl; intuition; auto with *.
   intros [xn xs] Ex.
   unfold dec_recip, Frac_dec_recip.
   simpl. case (decide_rel); simpl.
diff --git a/implementations/list.v b/implementations/list.v
index be3b191..c7d98d2 100644
--- a/implementations/list.v
+++ b/implementations/list.v
@@ -23,7 +23,7 @@ Section equivlistA_misc.
   Proof.
     split; intros E.
      inversion_clear E; auto. now destruct (proj1 (InA_nil eqA x)).
-    rewrite E. intuition.
+    rewrite E. intuition; auto with *.
   Qed.
 
   Lemma equivlistA_cons_nil x l : ¬equivlistA eqA (x :: l) [].
@@ -81,8 +81,8 @@ Section equivlistA_misc.
   Global Instance: Equivalence PermutationA.
   Proof.
     split.
-      intros l. induction l; intuition.
-     intros l₁ l₂. induction 1; eauto. apply permA_skip; intuition.
+      intros l. induction l; intuition; auto with *.
+     intros l₁ l₂. induction 1; eauto. apply permA_skip; intuition; auto with *.
     intros ???. now apply permA_trans.
   Qed.
 
@@ -92,7 +92,7 @@ Section equivlistA_misc.
 
   Lemma PermutationA_app_head l₁ l₂ k :
     PermutationA l₁ l₂ → PermutationA (k ++ l₁) (k ++ l₂).
-  Proof. intros. induction k. easy. apply permA_skip; intuition. Qed.
+  Proof. intros. induction k. easy. apply permA_skip; intuition; auto with *. Qed.
 
   Global Instance PermutationA_app :
     Proper (PermutationA ==> PermutationA ==> PermutationA) (@app A).
@@ -153,8 +153,8 @@ Section equivlistA_misc.
      intros. now rewrite equivlistA_nil_eq by now symmetry.
     intros l₂ Pl₂ E2.
     destruct (@InA_split _ eqA l₂ x) as [l₂h [y [l₂t [E3 ?]]]].
-     rewrite <-E2. intuition.
-    subst. transitivity (y :: l₁); [intuition |].
+     rewrite <-E2. intuition; auto with *.
+    subst. transitivity (y :: l₁); [intuition; auto with * |].
     apply PermutationA_cons_app, IHPl₁.
      now apply NoDupA_split with y.
     apply equivlistA_NoDupA_split with x y; intuition.
diff --git a/implementations/ne_list.v b/implementations/ne_list.v
index ae04b1a..79c74e9 100644
--- a/implementations/ne_list.v
+++ b/implementations/ne_list.v
@@ -95,10 +95,10 @@ Section contents.
   Definition Permutation (x y: L): Prop := ListPermutation x y.
 
   Global Instance: Equivalence Permutation.
-  Proof with intuition.
+  Proof.
    unfold Permutation.
-   split; repeat intro...
-   transitivity y...
+   split; repeat intro; auto with *.
+   transitivity y; auto with *.
   Qed.
 
   Global Instance: Proper (Permutation ==> ListPermutation) to_list.
diff --git a/implementations/polynomials.v b/implementations/polynomials.v
index 494698f..59ee288 100644
--- a/implementations/polynomials.v
+++ b/implementations/polynomials.v
@@ -59,7 +59,7 @@ Section contents.
   Proof. now destruct p. Qed.
 
   Instance: Reflexive poly_eq.
-  Proof with intuition. repeat intro. induction x... split... Qed.
+  Proof with intuition. repeat intro. induction x; auto with *. split; auto with *. Qed.
 
   Lemma poly_eq_cons :
     ∀ (a b : R) (p q : poly), (a = b /\ poly_eq p q) <-> poly_eq (a :: p) (b :: q).
diff --git a/orders/minmax.v b/orders/minmax.v
index 01df5c1..a0c9bd8 100644
--- a/orders/minmax.v
+++ b/orders/minmax.v
@@ -30,7 +30,7 @@ Section contents.
   Instance: LeftDistribute max min.
   Proof.
     intros x y z. unfold min, max, sort.
-    repeat case (decide_rel _); simpl; try solve [intuition].
+    repeat case (decide_rel _); simpl; try solve [intuition; auto with *].
      intros. apply (antisymmetry (≤)); [|easy]. now transitivity y; apply le_flip.
     intros. now apply (antisymmetry (≤)).
   Qed.
diff --git a/theory/ua_congruence.v b/theory/ua_congruence.v
index 7b84c43..cba9572 100644
--- a/theory/ua_congruence.v
+++ b/theory/ua_congruence.v
@@ -38,17 +38,17 @@ Section contents.
   Let lifted_normal := @op_type_equiv (sorts σ) v ve.
 
   Instance lifted_e_proper o: Proper ((=) ==> (=) ==> iff) (lifted_e o).
-  Proof with intuition.
+  Proof.
    induction o; simpl. intuition.
    repeat intro.
    unfold respectful.
    split; intros.
-    assert (x x1 = y x1). apply H0...
-    assert (x0 y1 = y0 y1). apply H1...
-    apply (IHo (x x1) (y x1) H4 (x0 y1) (y0 y1) H5)...
-   assert (x x1 = y x1). apply H0...
-   assert (x0 y1 = y0 y1). apply H1...
-   apply (IHo (x x1) (y x1) H4 (x0 y1) (y0 y1) H5)...
+    assert (x x1 = y x1). apply H0; auto with *.
+    assert (x0 y1 = y0 y1). apply H1; auto with *.
+    apply (IHo (x x1) (y x1) H4 (x0 y1) (y0 y1) H5); auto with *.
+   assert (x x1 = y x1). apply H0; auto with *.
+   assert (x0 y1 = y0 y1). apply H1; auto with *.
+   apply (IHo (x x1) (y x1) H4 (x0 y1) (y0 y1) H5); auto with *.
   Qed. (* todo: clean up *)
 
   (* With that out of the way, we show that there are two equivalent ways of stating compatibility with the
@@ -85,8 +85,8 @@ Section contents.
    clearbody f.
    induction (σ o)...
    simpl in *...
-   apply IHo0...
-   apply H1...
+   apply IHo0; intuition; auto with *.
+   apply H1; auto with *.
   Qed. (* todo: clean up *)
 
   Lemma eSub_eAlgebra: eSub → eAlgebra.
@@ -110,7 +110,7 @@ Section contents.
    simpl in *.
    repeat intro.
    unfold respectful in H0.
-   apply (IHo0 (λ b, f b (if b then x else y)))...
+   apply (IHo0 (λ b, f b (if b then x else y))); auto with *.
   Qed. (* todo: clean up *)
 
   Lemma back_and_forth: iffT eSub eAlgebra.
@@ -231,7 +231,7 @@ Section first_iso.
     exists o1...
    destruct X.
    apply (@op_closed_proper σ B _ _ _ image image_proper _ (o1 z) (o1 (f _ x))).
-    apply H3...
+    apply H3; auto with *.
    apply IHo0 with (o2 x)...
    apply _.
   Qed.
diff --git a/theory/ua_products.v b/theory/ua_products.v
index 20abb03..1f06f0d 100644
--- a/theory/ua_products.v
+++ b/theory/ua_products.v
@@ -198,9 +198,9 @@ Section categorical.
 
   Global Program Instance: IntroProduct c (product c) := λ H h a X i, h i a X.
 
-  Next Obligation. Proof with intuition.
+  Next Obligation. Proof.
    repeat constructor; try apply _.
-     intros ?? E ?. destruct h. simpl. rewrite E...
+     intros ?? E ?. destruct h. simpl. rewrite E; auto with *.
     intro o.
     pose proof (λ i, @preserves _ _ _ _ _ _ _ _ (proj2_sig (h i)) o) as H0.
     unfold product_ops, algebra_op.
@@ -208,8 +208,8 @@ Section categorical.
     set (o1 := varieties.variety_ops et H o) in *.
     change (∀i : I, Preservation et H (c i) (` (h i)) o1 (o0 i)) in H0.
     clearbody o0 o1. revert o0 o1 H0.
-    induction (et o); simpl...
-   apply (@product_algebra et I c)...
+    induction (et o); simpl; auto with *.
+   apply (@product_algebra et I c); auto with *.
   Qed.
 
   Global Instance: Product c (product c).
diff --git a/theory/ua_subalgebra.v b/theory/ua_subalgebra.v
index 93c5736..b27e166 100644
--- a/theory/ua_subalgebra.v
+++ b/theory/ua_subalgebra.v
@@ -16,12 +16,12 @@ Section subalgebras.
     end.
 
   Global Instance op_closed_proper: ∀ `{∀ s, Proper ((=) ==> iff) (P s)} o, Proper ((=) ==> iff) (@op_closed o).
-  Proof with intuition.
+  Proof.
    induction o; simpl; intros x y E.
-    rewrite E...
+    rewrite E; auto with *.
    split; intros.
-    apply (IHo (x z))... apply E...
-   apply (IHo _ (y z))... apply E...
+    apply (IHo (x z)); auto with *. apply E; auto with *.
+   apply (IHo _ (y z)); auto with *. apply E; auto with *.
   Qed.
 
   Class ClosedSubset: Prop :=
diff --git a/theory/ua_subalgebraT.v b/theory/ua_subalgebraT.v
index 284266c..f4e55df 100644
--- a/theory/ua_subalgebraT.v
+++ b/theory/ua_subalgebraT.v
@@ -28,10 +28,10 @@ Section subalgebras.
     intuition.
    split; intros...
     apply (IHo (x z))...
-    apply E...
-   apply (IHo (y z))...
+    apply E; auto with *.
+   apply (IHo (y z)); auto with *.
    symmetry.
-   apply E...
+   apply E; auto with *.
   Qed.
 
   Class ClosedSubset: Type :=
diff --git a/theory/ua_subvariety.v b/theory/ua_subvariety.v
index 59fd001..27aa720 100644
--- a/theory/ua_subvariety.v
+++ b/theory/ua_subvariety.v
@@ -33,23 +33,23 @@ Section contents.
      transitivity x0...
     transitivity x1...
     transitivity y0...
-   assert (∀ u, x u = y u). intros. apply U...
+   assert (∀ u, x u = y u). intros. apply U; auto with *.
    split; repeat intro.
     apply -> (IHo (x u) (y u) (H1 u) (x0 (proj1_sig u)))...
-    apply K...
+    apply K; auto with *.
    apply <- (IHo (x u) (y u) (H1 u) (x0 (proj1_sig u)))...
-   apply K...
+   apply K; auto with *.
   Qed.
 
   Lemma heq_eval vars {o} (t: T et o): heq (eval et vars t) (eval et (Pvars vars) t).
   Proof with intuition.
    induction t; simpl...
-     unfold Pvars...
+     unfold Pvars; auto with *.
     simpl in IHt1.
     generalize (IHt1 (eval et vars t3)). clear IHt1.
     apply heq_proper.
      pose proof (@eval_proper et (carrier P) _ _ _ nat (ne_list.cons y t1)).
-     apply H1; try intro...
+     apply H1; try intro; auto with *.
     pose proof (@eval_proper et A _ _ _ nat (ne_list.cons y t1)).
     apply H1...
     unfold heq in IHt2. (* todo: this wasn't needed in a previous Coq version *)
diff --git a/theory/ua_term_monad.v b/theory/ua_term_monad.v
index 9c5360b..d97223d 100644
--- a/theory/ua_term_monad.v
+++ b/theory/ua_term_monad.v
@@ -75,10 +75,10 @@ Section contents.
       geneq x y → geneq (gen_bind_aux x0 x) (gen_bind_aux y0 y))...
    revert s' y H.
    induction x.
-     destruct y... simpl in *.
+     destruct y; auto with *. simpl in *.
      destruct a, a1. apply E'...
     simpl in *. destruct y... destruct y...
-    simpl in *... destruct y...
+    simpl in *... destruct y; auto with *.
   Qed.
 
   (* return: *)
diff --git a/varieties/closed_terms.v b/varieties/closed_terms.v
index a119dd1..a87034d 100644
--- a/varieties/closed_terms.v
+++ b/varieties/closed_terms.v
@@ -156,9 +156,9 @@ Section contents.
      do 2 rewrite eval_is_close.
      do 2 rewrite <- subst_eval.
      apply Q. clear Q.
-     induction entailment_premises; simpl...
+     induction entailment_premises; simpl; auto with *.
      do 2 rewrite subst_eval.
-     do 2 rewrite <- eval_is_close...
+     do 2 rewrite <- eval_is_close; auto with *.
     Qed.
 
     Instance: ∀ a, Setoid_Morphism (@eval_in_other (ne_list.one a)).
diff --git a/varieties/empty.v b/varieties/empty.v
index ef793b5..9bf5c1a 100644
--- a/varieties/empty.v
+++ b/varieties/empty.v
@@ -21,11 +21,11 @@ Proof. intros []. Qed.
 Instance implementation: AlgebraOps sig carriers := λ o, False_rect _ o.
 
 Global Instance: Algebra sig _.
-Proof. constructor; intuition. Qed.
+Proof. constructor; intuition; auto with *. Qed.
 
 #[global]
 Instance variety: InVariety theory carriers.
-Proof. constructor; intuition. Qed.
+Proof. constructor; intuition; auto with *. Qed.
 
 Definition Object := varieties.Object theory.
 Definition object: Object := varieties.object theory carriers.
diff --git a/varieties/setoids.v b/varieties/setoids.v
index 6874941..87177f5 100644
--- a/varieties/setoids.v
+++ b/varieties/setoids.v
@@ -21,10 +21,10 @@ Section from_instance.
   Instance: AlgebraOps sig carriers := λ o, False_rect _ o.
 
   Instance: Algebra sig carriers.
-  Proof. constructor; intuition. Qed.
+  Proof. constructor; intuition; auto with *. Qed.
 
   Instance: InVariety theory carriers.
-  Proof. constructor; intuition. Qed.
+  Proof. constructor; intuition; auto with *. Qed.
 
   Definition object: varieties.Object theory := varieties.object theory (λ _, A).