diff --git a/algebra/CMonoids.v b/algebra/CMonoids.v
index d2f89e4e..85abb211 100644
--- a/algebra/CMonoids.v
+++ b/algebra/CMonoids.v
@@ -253,12 +253,12 @@ Proof.
   astepl ((Inv f iso_imp_bij) (f a' [+] f b')).
   astepl ((Inv f iso_imp_bij) ( f ( a'[+] b'))).
    set (H3:= (inv2 M1 M2 f iso_imp_bij (a'[+]b'))).
-   astepl (a'[+]b'). astepr (a'[+] b'). intuition.
+   astepl (a'[+]b'). astepr (a'[+] b'). intuition; auto with *.
    set (H4:=(inv2 M1 M2 f iso_imp_bij a')).
    apply csbf_wd.
-    astepr (Inv f iso_imp_bij (f a')); intuition.
-   astepr (Inv f iso_imp_bij (f b')).  set (H5:= (inv2 M1 M2 f iso_imp_bij b')); intuition.
-   intuition.
+    astepr (Inv f iso_imp_bij (f a')); intuition; auto with *.
+   astepr (Inv f iso_imp_bij (f b')).  set (H5:= (inv2 M1 M2 f iso_imp_bij b')); intuition; auto with *.
+   intuition; auto with *.
  apply Inv_bij.
 Qed.
 
@@ -335,11 +335,11 @@ Proof.
  induction s.
   simpl.
   replace (k+0) with k.
-   intuition.
+   intuition; auto with *.
   intuition.
  simpl.
  replace (k+((l-k)+s*(l-k)))  with (l + s*(l-k)).
-  2:intuition.
+  2:intuition; auto with *.
  set (H1:= (power_plus M u l (s*(l-k)))).
  astepr  (csbf_fun (csg_crr (cm_crr M)) (csg_crr (cm_crr M))
    (csg_crr (cm_crr M)) (csg_op (c:=cm_crr M)) (power_CMonoid u l) (power_CMonoid u (s * (l - k)))).
@@ -374,7 +374,7 @@ Proof.
  intros H4.
  set (H6:=(Z_div_mod_eq_full (n-k)(l-k))).
  cut (((n - k) mod (l - k))= (n-k)%Z -((l - k) * ((n - k) / (l - k))))%Z.
-  2:intuition.
+  2:intuition; auto with *.
  set (H7:=(mod_nat_correct (n-k) (l-k) H2)).
  intro H8.
  cut {s:nat | (mod_nat (n-k)(l-k) H2)=(n-k)-s*(l-k) and s*(l-k)<=(n-k)}.
@@ -391,7 +391,7 @@ Proof.
    rewrite -> (power_plus M  u  (k+(s*(l-k))) ((n-k)-s*(l-k))).
    rewrite -> (power_plus M u k (n-k-s*(l-k))).
    setoid_replace (power_CMonoid u (k + s * (l - k))) with (power_CMonoid u k). now reflexivity.
-  unfold canonical_names.equiv. now intuition. 
+  unfold canonical_names.equiv. now intuition; auto with *. 
   cut (n=k+(n-k)).
    intro H10.
    cut (n=((k+(n-k))+(s*(l-k)-s*(l-k)))).
@@ -408,18 +408,18 @@ Proof.
     intro H11.
     rewrite H11.
     now intuition.
-   now intuition.
+   now intuition; auto with *.
   cut (n=n+(k-k)).
    intro H10.
    cut (n+(k-k)=k+(n-k)).
     intro H11.
     now rewrite<- H10 in H11.
    apply minus3.
-   split; now intuition.
+   split; now intuition; auto with *.
   cut ((k-k)=0).
    intro H10.
    now rewrite H10.
-  now intuition.
+  now intuition; auto with *.
  simpl.
  cut (l-k>0).
   intro H9.
@@ -435,17 +435,17 @@ Proof.
    elim H10'.
    clear H10'.
    intros H10' H10''.
-   3:intuition.
+   3:intuition; auto with *.
   cut ((n-k)= q*(l-k)+ (mod_nat (n-k)(l-k) H2)).
    intro H11.
-   intuition.
+   intuition; auto with *.
   cut (r= (mod_nat (n-k)(l-k)H2)).
    intro H11.
    now rewrite<- H11.
   simpl.
   cut ((Z_of_nat r)=(mod_nat (n - k) (l - k) H2)).
    intro H11.
-   intuition.
+   intuition; auto with *.
   rewrite<- H7.
   apply nat_Z_div with (n-k) q (l-k) ((Z_of_nat n - Z_of_nat k) / (Z_of_nat l - Z_of_nat k))%Z.
      exact H10'.
@@ -459,17 +459,17 @@ Proof.
      set (H16:=(inj_minus1 n k H14)).
      rewrite H16.
      exact H6.
-    intuition.
-   intuition.
+    intuition; auto with *.
+   intuition; auto with *.
   set (H17:=(Z_mod_lt (Z_of_nat (n-k)) (Z_of_nat (l-k)))).
-  intuition.
+  intuition; auto with *.
  elim H10.
  clear H10.
  intros r H10.
  elim H10.
  clear H10.
  intros H10 H10'.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma cyc_imp_comm: forall (M:CMonoid)(H:(cyclic M)), (commutes (@csg_op M)).
@@ -491,7 +491,7 @@ Proof.
  replace (nx+ny) with (ny+nx).
   rewrite -> (power_plus M c0 ny nx).
   now apply eq_reflexive.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma weakly_inj1:
@@ -544,12 +544,12 @@ Proof.
      split.
       intuition.
      right.
-     intuition.
-    intuition.
+     intuition; auto with *.
+    intuition; auto with *.
    clear orex.
    intro orex.
-   intuition.
-  intuition.
+   intuition; auto with *.
+  intuition auto with *.
  clear H5.
  intro H5.
  cut False.
@@ -587,13 +587,13 @@ Proof.
      split.
       intuition.
      right.
-     intuition.
-    intuition.
+     intuition auto with *.
+    intuition auto with *.
    clear orex.
    intro orex.
-   intuition.
-  intuition.
- intuition.
+   intuition; auto with *.
+  intuition auto with *.
+ intuition; auto with *.
 
 Qed.
 
@@ -716,14 +716,14 @@ Proof.
  simpl.
  split.
   split.
-   intuition.
+   intuition; auto with *.
   intros a b.
   case a.
   intros a0 a1.
   case b.
   intros b0 b1.
   simpl.
-  intuition.
+  intuition; auto with *.
  unfold bijective.
  split.
   unfold injective.
@@ -741,7 +741,7 @@ Proof.
  intros a0 a1.
  exists (pairT a1 a0).
  simpl.
- intuition.
+ intuition; auto with *.
 Qed.
 
 End p71E2b2.
@@ -768,7 +768,7 @@ Proof.
  unfold eq_fun in |- *.
  unfold id_un_op in |- *.
  simpl in |- *.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma id_is_lft_unit :
@@ -781,7 +781,7 @@ Proof.
  unfold eq_fun in |- *.
  unfold id_un_op in |- *.
  simpl in |- *.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Definition FS_is_CMonoid (A : CSetoid) :=
@@ -813,7 +813,7 @@ Proof.
  induction a.
   apply eq_fm_reflexive.
  simpl.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Section Th12.
@@ -835,7 +835,7 @@ Proof.
   simpl.
   intuition.
  simpl.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma nil_is_lft_unit: (is_lft_unit (app_as_csb_fun A) (empty_word A)).
@@ -847,7 +847,7 @@ Proof.
   simpl.
   intuition.
  simpl.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Definition free_monoid_is_CMonoid:
@@ -943,7 +943,7 @@ Proof.
  unfold Dbrack.
  exists (@nil M).
  simpl.
- intuition.
+ intuition; auto with *.
 Qed.
 
 
@@ -958,7 +958,7 @@ Proof.
  simpl.
  astepr (a [+] ( (cm_Sum k)[+](cm_Sum l))).
  apply csbf_wd_unfolded.
-  intuition.
+  intuition; auto with *.
  exact IHk.
 Qed.
 
@@ -986,7 +986,7 @@ Qed.
 Lemma cm_Sum_units (a: list M): (forall x, In x a -> x [=] [0]) -> cm_Sum a [=] [0].
 Proof with intuition.
  clear D.
- induction a. intuition.
+ induction a. intuition; auto with *.
  intros E.
  simpl.
  rewrite IHa...
diff --git a/algebra/COrdFields2.v b/algebra/COrdFields2.v
index 26b6a87a..243a7039 100644
--- a/algebra/COrdFields2.v
+++ b/algebra/COrdFields2.v
@@ -739,7 +739,7 @@ Proof.
   astepr ((Two:R)[^]S n).
   astepl (([1]:R)[^]S n).
   apply nexp_resp_less.
-    intuition.
+    intuition; auto with *.
    apply less_leEq.
    apply pos_one.
   apply one_less_two.
diff --git a/algebra/CSemiGroups.v b/algebra/CSemiGroups.v
index 0b83eb1f..a765aef0 100644
--- a/algebra/CSemiGroups.v
+++ b/algebra/CSemiGroups.v
@@ -378,7 +378,7 @@ Proof.
   intros x y.
   apply eq_fm_reflexive.
  simpl.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Definition Astar_as_CSemiGroup:=
diff --git a/algebra/CSetoidFun.v b/algebra/CSetoidFun.v
index 41c23795..43fd5464 100644
--- a/algebra/CSetoidFun.v
+++ b/algebra/CSetoidFun.v
@@ -231,7 +231,7 @@ Proof.
  simpl in |- *.
  unfold eq_fun in |- *.
  simpl in |- *.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Section unary_and_binary_function_composition.
@@ -579,7 +579,7 @@ Proof.
   simpl.
   intuition.
  simpl.
- intuition.
+ intuition; auto with *.
 Qed.
 
 End p66E2b4.
diff --git a/liouville/Liouville.v b/liouville/Liouville.v
index a50e7d91..e046cbd0 100644
--- a/liouville/Liouville.v
+++ b/liouville/Liouville.v
@@ -239,8 +239,8 @@ Proof.
  unfold Z.abs.
  destruct p.
    destruct Hap; reflexivity.
-  simpl; unfold Qle; simpl; intuition.
- simpl; unfold Qle; simpl; intuition.
+  simpl; unfold Qle; simpl; intuition; auto with *.
+ simpl; unfold Qle; simpl; intuition; auto with *.
 Qed.
 
 Lemma Liouville_lemma5 : forall (p : Z_as_CRing) (q : positive), (zx2qx P) ! (p#q)%Q [#] [0] ->
diff --git a/logic/CLogic.v b/logic/CLogic.v
index 168472a6..55c2df1c 100644
--- a/logic/CLogic.v
+++ b/logic/CLogic.v
@@ -1610,7 +1610,7 @@ Lemma CForall_indexed {A} (P: A -> Type) (l: list A): CForall P l ->
 Proof.
  intros X i.
  revert l X.
- induction i; destruct l; simpl in *; intuition; exfalso; inversion H.
+ induction i; destruct l; simpl in *; intuition; auto with *; exfalso; inversion H.
 Qed.
 
 Lemma CForall_map {A B} (P: B -> Type) (f: A -> B) (l: list A):
@@ -1639,24 +1639,24 @@ Qed.
 
 Lemma CNoDup_indexed {T} (R: T -> T -> Type) (Rsym: Csymmetric _ R) (l: list T) (d: T): CNoDup R l ->
   forall i j, (i < length l)%nat -> (j < length l)%nat -> i <> j -> R (nth i l d) (nth j l d).
-Proof with intuition.
- induction l; simpl...
-  exfalso...
+Proof.
+ induction l; simpl; intuition.
+  exfalso; auto with *.
  destruct i.
-  destruct j...
-  apply (CForall_indexed (R a) l)...
- destruct j...
+  destruct j; intuition.
+  apply (CForall_indexed (R a) l); auto with *.
+ destruct j; auto with *.
  apply Rsym.
- apply (CForall_indexed (R a) l)...
+ apply (CForall_indexed (R a) l); auto with *.
 Qed.
 
 Lemma CNoDup_map {A B: Type} (R: B -> B -> Type) (f: A -> B):
   forall l, CNoDup (fun x y => R (f x) (f y)) l  IFF  CNoDup R (map f l).
-Proof with auto; intuition.
- induction l; simpl...
+Proof.
+ induction l; simpl; auto; intuition; auto with *.
  split; intro; split.
     apply IHl, X.
-   apply CForall_map...
+   apply CForall_map; auto; intuition.
   apply IHl, X.
- apply CForall_map...
+ apply CForall_map; auto; intuition.
 Qed.
diff --git a/logic/CornBasics.v b/logic/CornBasics.v
index 75bfc556..dd044746 100644
--- a/logic/CornBasics.v
+++ b/logic/CornBasics.v
@@ -161,7 +161,7 @@ Lemma minus3:forall (a b c:nat),(c<=b<=a)-> a+(b-c)=b+(a-c).
 Proof.
  intros a b d H.
  cut  ((Z_of_nat a) + ((Z_of_nat b) - (Z_of_nat d)) = (Z_of_nat b) + ((Z_of_nat a) - (Z_of_nat d)))%Z.
-  2:intuition.
+  2:intuition; auto with *.
  intro H1.
  elim H.
  intros H2 H3.
@@ -169,10 +169,10 @@ Proof.
  rewrite<- H4 in H1.
  cut (d <=a).
   intro H5.
-  2:intuition.
+  2:intuition; auto with *.
  set (H6:=(inj_minus1 a d H5)).
  rewrite<- H6 in H1.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma minus4:forall (a b c d:nat), (d<=c<=b)->
@@ -182,17 +182,17 @@ Proof.
  cut (((Z_of_nat a)+(Z_of_nat b))+((Z_of_nat c0)-(Z_of_nat d))=
    ((Z_of_nat a)+(Z_of_nat c0))+((Z_of_nat b)-(Z_of_nat d)))%Z.
   intro H0.
-  2:intuition.
+  2:intuition; auto with *.
  elim H.
  intros H1 H2.
  set (H3:=(inj_minus1 c0 d H1)).
  rewrite<- H3 in H0.
  cut (d<=b).
-  2:intuition.
+  2:intuition; auto with *.
  intro H4.
  set (H5:=(inj_minus1 b d H4)).
  rewrite<- H5 in H0.
- intuition.
+ intuition; auto with *.
 Qed.
 
 (** The power function does not exist in the standard library *)
@@ -367,21 +367,21 @@ Lemma surj_eq:forall (n m:nat),
 ((Z_of_nat n)=(Z_of_nat m))%Z -> n=m.
 Proof.
  intros n m.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma surj_le:forall (n m:nat),
 ((Z_of_nat n)<=(Z_of_nat m))%Z -> n<=m.
 Proof.
  intros n m.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma surj_lt:forall (n m:nat),
 ((Z_of_nat n)<(Z_of_nat m))%Z -> n<m.
 Proof.
  intros n m.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma surj_not:forall (n m:nat),
@@ -395,7 +395,7 @@ Lemma lt_lt_minus:forall(q p l:nat),
 q<l -> p<q -> p+(l-q)<l.
 Proof.
  intros q p l H H0.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma inject_nat_convert :
diff --git a/metric2/Classified.v b/metric2/Classified.v
index a2f6606e..4c22ec25 100644
--- a/metric2/Classified.v
+++ b/metric2/Classified.v
@@ -210,7 +210,7 @@ Section genball.
   Qed.
 
   Instance genball_Proper: Proper ((=) ==> (=) ==> (=) ==> iff) genball.
-  Proof with auto; intuition.
+  Proof with auto; intuition; auto with *.
    unfold genball.
    intros u e' E.
    destruct u, e'.
@@ -226,7 +226,7 @@ Section genball.
        exfalso. revert q2. rewrite <- E, q1. apply Qlt_irrefl.
       intros ?? A ?? B. rewrite A, B...
      repeat intro...
-    intuition.
+    intuition; auto with *.
    repeat intro.
    reflexivity.
   Qed.
@@ -250,7 +250,7 @@ Proof. intros; now apply genball_Proper. Qed.
    repeat intro.
    unfold genball.
    destruct q...
-   destruct Qdec_sign as [[|]|]; intuition...
+   destruct Qdec_sign as [[|]|]; intuition; auto with *.
    apply (Qlt_not_le q 0)...
   Qed.
 
diff --git a/metric2/list_separates.v b/metric2/list_separates.v
index 4f498df8..0ca7a6ec 100644
--- a/metric2/list_separates.v
+++ b/metric2/list_separates.v
@@ -36,7 +36,7 @@ Qed.
 #[global]
 Instance separates_Proper {A}:
   Proper (@Permutation _ ==> SetoidPermutation (pair_rel eq (@Permutation _))) (@separates A).
-Proof with simpl; auto; intuition.
+Proof with simpl; auto; intuition; auto with *.
  intros ?? P.
  induction P...
      3:eauto.
diff --git a/metrics/CMetricSpaces.v b/metrics/CMetricSpaces.v
index 12d64f5f..a20ff07e 100644
--- a/metrics/CMetricSpaces.v
+++ b/metrics/CMetricSpaces.v
@@ -578,7 +578,7 @@ Lemma nz : forall n m : nat, n <= Nat.max n m.
 Proof.
  intro n.
  intro m.
- intuition.
+ intuition; auto with *.
 Qed.
 (* end hide *)
 
diff --git a/metrics/CPMSTheory.v b/metrics/CPMSTheory.v
index 38a3dd8d..a920b840 100644
--- a/metrics/CPMSTheory.v
+++ b/metrics/CPMSTheory.v
@@ -132,7 +132,7 @@ Proof.
  intros.
  right.
  rewrite b.
- intuition.
+ intuition; auto with *.
 Qed.
 
 (**
@@ -660,8 +660,8 @@ Proof.
    apply leEq_transitive with (xj[-d]from_SubPsMetricSpace X P x0).
     apply eq_imp_leEq.
     apply csbf_wd_unfolded.
-     intuition.
-    intuition.
+     intuition; auto with *.
+    intuition; auto with *.
    exact q.
   apply plus_resp_leEq.
   apply leEq_transitive with (from_SubPsMetricSpace X P x[-d]xj).
diff --git a/metrics/CPseudoMSpaces.v b/metrics/CPseudoMSpaces.v
index daf8ac66..870fc473 100644
--- a/metrics/CPseudoMSpaces.v
+++ b/metrics/CPseudoMSpaces.v
@@ -290,7 +290,7 @@ Proof.
  unfold Zero_fun in |- *.
  simpl in |- *.
  unfold zero_fun in |- *.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma zero_fun_nneg : forall X : CSetoid, nneg (Zero_fun X).
@@ -302,7 +302,7 @@ Proof.
  simpl in |- *.
  unfold zero_fun in |- *.
  apply eq_imp_leEq.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma zero_fun_pos_imp_ap : forall X : CSetoid, pos_imp_ap (Zero_fun X).
diff --git a/metrics/ContFunctions.v b/metrics/ContFunctions.v
index f452ab33..85280603 100644
--- a/metrics/ContFunctions.v
+++ b/metrics/ContFunctions.v
@@ -183,7 +183,7 @@ Proof.
   apply recip_resp_less.
    unfold Snring in |- *.
    apply nring_pos.
-   intuition.
+   intuition; auto with *.
   apply nat_less_bin_nexp.
  unfold one_div_succ in |- *.
  unfold Snring in |- *.
diff --git a/metrics/IR_CPMSpace.v b/metrics/IR_CPMSpace.v
index a31b0869..b778e4c9 100644
--- a/metrics/IR_CPMSpace.v
+++ b/metrics/IR_CPMSpace.v
@@ -277,14 +277,14 @@ Proof.
       apply great_nexp_resp_le.
        apply less_leEq.
        apply one_less_two.
-      intuition.
+      intuition; auto with *.
      apply ax_d_nneg.
      apply CPsMetricSpace_is_CPsMetricSpace.
     apply mult_resp_leEq_rht.
      apply great_nexp_resp_le.
       apply less_leEq.
       apply one_less_two.
-     intuition.
+     intuition; auto with *.
     apply ax_d_nneg.
     apply CPsMetricSpace_is_CPsMetricSpace.
    apply eq_imp_leEq.
@@ -350,7 +350,7 @@ Proof.
     astepr (Two:IR).
     apply less_leEq.
     apply one_less_two.
-   intuition.
+   intuition; auto with *.
   apply leEq_transitive with ((OneR[/] Two:IR[//]H1)[^]S n[+]([1][/] Two:IR[//]H1)[^]S n).
    apply plus_resp_leEq_lft.
    apply less_leEq.
@@ -374,7 +374,7 @@ Proof.
     astepr (Two:IR).
     apply less_leEq.
     apply one_less_two.
-   intuition.
+   intuition; auto with *.
   apply eq_imp_leEq.
   astepl ((Two:IR)[*]([1][/] Two:IR[//]H1)[^]S n).
   astepl ((Two:IR)[*]([1][^]S n[/] (Two:IR)[^]S n[//]nexp_resp_ap_zero (S n) H1)).
@@ -442,7 +442,7 @@ Proof.
      apply less_leEq.
      apply one_less_two.
     rational.
-   intuition.
+   intuition; auto with *.
   apply leEq_transitive with ((OneR[/] [0][+][1][+][1][//]H1)[^]S n[+]
     ([1][/] [0][+][1][+][1][//]H1)[^]S n).
    apply plus_resp_leEq_lft.
@@ -467,7 +467,7 @@ Proof.
      apply less_leEq.
      apply one_less_two.
     rational.
-   intuition.
+   intuition; auto with *.
   apply eq_imp_leEq.
   astepl ((Two:IR)[*]([1][/] [0][+][1][+][1][//]H1)[^]S n).
   astepr ((OneR[/] [0][+][1][+][1][//]H1)[^]n).
@@ -494,4 +494,5 @@ Proof.
  rational.
 Qed.
 
+
 End Addition.
diff --git a/metrics/Prod_Sub.v b/metrics/Prod_Sub.v
index 47c5e087..cbed5c0e 100644
--- a/metrics/Prod_Sub.v
+++ b/metrics/Prod_Sub.v
@@ -398,14 +398,14 @@ Proof.
    apply rev_tri_ineq.
   apply csf_wd.
   apply cg_minus_wd.
-   intuition.
+   intuition; auto with *.
   apply ax_d_com.
   apply CPsMetricSpace_is_CPsMetricSpace.
  apply csf_wd.
  apply cg_minus_wd.
   apply ax_d_com.
   apply CPsMetricSpace_is_CPsMetricSpace.
- intuition.
+ intuition; auto with *.
 Qed.
 
 
diff --git a/model/Zmod/Cmod.v b/model/Zmod/Cmod.v
index 88801695..59b901a2 100644
--- a/model/Zmod/Cmod.v
+++ b/model/Zmod/Cmod.v
@@ -63,9 +63,9 @@ Proof.
  cut False.
   intuition.
  cut (Zneg p < 0)%Z.
-  intuition.
+  intuition; auto with *.
  unfold Z.lt.
- intuition.
+ intuition; auto with *.
 Qed.
 
 
@@ -98,7 +98,7 @@ Proof.
  simpl.
  intro x.
  set (H1:= (inject_nat_convert x)).
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma  nat_Z_div:forall (a b c r:nat)(b' r':Z),
@@ -107,7 +107,7 @@ Proof.
  intros a b c0 r b' r' H H1 H2 H3.
  cut (c0>0)%Z.
   intro H5.
-  2:intuition.
+  2:intuition; auto with *.
  set (H4:=(Z_div_mod_eq_full (Z_of_nat a) (Z_of_nat c0))).
  cut ((Z_of_nat a mod (Z_of_nat c0))%Z = r').
   intro H6.
@@ -124,12 +124,12 @@ Proof.
   rewrite H9.
   rewrite H8.
   apply Zmod_small.
-   intuition.
+   intuition; auto with *.
   intuition.
  rewrite H2.
  replace (Z_of_nat c0 * b' + r')%Z with ( b'*Z_of_nat c0 + r')%Z.
-  2:intuition.
+  2:intuition; auto with *.
  set (H8:= (Zmod_cancel_multiple c0 r' b' H5)).
  rewrite H8.
- apply Zmod_small; intuition.
+ apply Zmod_small; intuition; auto with *.
 Qed.
diff --git a/model/Zmod/IrrCrit.v b/model/Zmod/IrrCrit.v
index e9fec357..6ffc696b 100644
--- a/model/Zmod/IrrCrit.v
+++ b/model/Zmod/IrrCrit.v
@@ -155,7 +155,7 @@ Hint Resolve mult_zero : algebra.
 
 Lemma fp_resp_zero : zxfpx(cpoly_zero Z_as_CRing)[=](cpoly_zero fp).
 Proof.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma fpx_resp_mult_cr : forall (c:Z_as_CRing)(f:zx),
@@ -163,13 +163,13 @@ Lemma fpx_resp_mult_cr : forall (c:Z_as_CRing)(f:zx),
   (zxfpx (cpoly_mult_cr_cs _ f c)).
 Proof.
  induction f as [|c0 f].
-  intuition.
+  intuition; auto with *.
  astepr (zxfpx ((c[*]c0)[+X*](cpoly_mult_cr_cs _ f c))).
  astepr ((zfp (c[*]c0))[+X*](zxfpx (cpoly_mult_cr_cs _ f c))).
  astepr (((zfp c)[*](zfp c0))[+X*](zxfpx (cpoly_mult_cr_cs _ f c))).
  astepr (((zfp c)[*](zfp c0))[+X*](cpoly_mult_cr_cs fp (zxfpx f) (zfp c))).
  astepr (cpoly_mult_cr_cs fp ((zfp c0)[+X*](zxfpx f)) (zfp c)).
- intuition.
+ intuition; auto with *.
 Qed.
 
 #[global]
@@ -180,9 +180,9 @@ Lemma fpx_resp_plus :  forall f g:zx,
   (zxfpx (cpoly_plus_op _ f g)).
 Proof.
  induction f as [|c f].
-  intuition.
+  intuition; auto with *.
  induction g as [|c0 g].
-  intuition.
+  intuition; auto with *.
  astepl (cpoly_plus fp (zxfpx (c[+X*]f)) (zxfpx (c0[+X*]g))).
  astepr (zxfpx (cpoly_plus_op _ (c[+X*]f) (c0[+X*]g))).
  astepr (zxfpx ((c[+]c0)[+X*](cpoly_plus_op _ f g))).
@@ -203,7 +203,7 @@ Proof.
   astepl (cpoly_mult_op fp (cpoly_zero fp)(zxfpx g)).
   astepl (cpoly_zero fp).
   astepr (zxfpx (cpoly_zero Z_as_CRing)).
-  astepr (cpoly_zero fp); intuition.
+  astepr (cpoly_zero fp); intuition; auto with *.
  induction g as [|c0 g].
   astepl (cpoly_mult_op fp (zxfpx (c[+X*]f)) (cpoly_zero fp)).
   astepl (cpoly_zero fp).
@@ -231,7 +231,7 @@ Proof.
    (([0]:fp)[+X*](zxfpx (cpoly_mult_op _ f (c0[+X*]g))))).
  astepl ((zfp (c[*]c0)[+]([0]:fp))[+X*](cpoly_plus_op fp
    (zxfpx (cpoly_mult_cr_cs _ g c)) (zxfpx (cpoly_mult_op _ f (c0[+X*]g))))).
- intuition.
+ intuition; auto with *.
 Qed.
 
 #[global]
@@ -241,9 +241,9 @@ Lemma fpx_resp_coef : forall (f:zx)(n:nat), (zfp (nth_coeff n f))
   [=] (nth_coeff n (zxfpx f)).
 Proof.
  induction f.
-  intuition.
+  intuition; auto with *.
  induction n.
-  intuition.
+  intuition; auto with *.
  astepl (zfp (nth_coeff n f)).
  astepr (nth_coeff n (zxfpx f)).
  apply (IHf n).
@@ -281,17 +281,17 @@ Proof.
  unfold monic.
  split.
   astepl (zfp (nth_coeff m f)).
-  assert ([1][=]nth_coeff m f); intuition.
+  assert ([1][=]nth_coeff m f); intuition; auto with *.
   simpl in H.
   rewrite <- H.
-  intuition.
+  intuition; auto with *.
  red.
  intros.
  astepl (zfp (nth_coeff m0 f)).
- assert ([0][=]nth_coeff m0 f); intuition.
+ assert ([0][=]nth_coeff m0 f); intuition; auto with *.
  simpl in H0.
  rewrite <- H0.
- intuition.
+ intuition; auto with *.
 Qed.
 
 #[global]
@@ -309,11 +309,11 @@ Proof.
  intros Hfok Hfred2; elim Hfred2.
  intros g Hgok Hfred3; elim Hfred3.
  intros h Hhok Hfgh; unfold reducible.
- intuition.
+ intuition; auto with *.
  exists (zxfpx g).
-  intuition.
+  intuition; auto with *.
  exists (zxfpx h).
-  intuition.
+  intuition; auto with *.
  astepr (zxfpx (cpoly_mult_op _ g h)).
  apply fpxeq_wd.
  exact Hfgh.
diff --git a/model/Zmod/ZBasics.v b/model/Zmod/ZBasics.v
index 9cbdf08b..08c76cbb 100644
--- a/model/Zmod/ZBasics.v
+++ b/model/Zmod/ZBasics.v
@@ -257,7 +257,7 @@ Section zineq.
 Lemma Zgt_Zge: forall (n m:Z), (n>m)%Z -> (n>=m)%Z.
 Proof.
  intros n m.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma Zle_antisymm : forall a b : Z, (a >= b)%Z -> (b >= a)%Z -> a = b.
@@ -519,7 +519,7 @@ Qed.
 Lemma Zcompat_lt_plus: forall (n m p:Z),(n < m)%Z-> (p+n < p+m)%Z.
 Proof.
  intros n m p.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Transparent Zplus.
@@ -531,7 +531,7 @@ Proof.
  simpl.
  set (H:=(succ_nat m)).
  rewrite H.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Opaque Zplus.
diff --git a/model/monoids/Zmonoid.v b/model/monoids/Zmonoid.v
index a9d0a6ff..2e1886a9 100644
--- a/model/monoids/Zmonoid.v
+++ b/model/monoids/Zmonoid.v
@@ -68,7 +68,7 @@ Proof.
  simpl.
  split.
   reflexivity.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Definition Z_is_CMonoid := Build_is_CMonoid
diff --git a/model/setoids/Nfinsetoid.v b/model/setoids/Nfinsetoid.v
index dc864f2d..c1c7ed61 100644
--- a/model/setoids/Nfinsetoid.v
+++ b/model/setoids/Nfinsetoid.v
@@ -121,7 +121,7 @@ Proof.
  red in |- *.
  unfold not in |- *.
  unfold Not in |- *.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Definition less (n : nat) :=
diff --git a/model/setoids/Zfinsetoid.v b/model/setoids/Zfinsetoid.v
index 6620e0ad..47e6a0b3 100644
--- a/model/setoids/Zfinsetoid.v
+++ b/model/setoids/Zfinsetoid.v
@@ -122,7 +122,7 @@ Proof.
  red in |- *.
  unfold not in |- *.
  unfold Not in |- *.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Definition Zless (n : Z) :=
diff --git a/model/setoids/decsetoid.v b/model/setoids/decsetoid.v
index b2e6812d..2188fa79 100644
--- a/model/setoids/decsetoid.v
+++ b/model/setoids/decsetoid.v
@@ -40,8 +40,8 @@ Section contents.
   Instance ap_apart: Apartness ap.
   Proof with auto.
    apply Build_Apartness.
-      do 2 intro. intuition.
-     do 4 intro. intuition.
+      do 2 intro. intuition; auto with *.
+     do 4 intro. intuition; auto with *.
     intros x y H z.
     destruct (eq_dec x z)...
     destruct (eq_dec z y)...
diff --git a/model/structures/Nsec.v b/model/structures/Nsec.v
index 24994f1e..bf485b15 100644
--- a/model/structures/Nsec.v
+++ b/model/structures/Nsec.v
@@ -237,7 +237,7 @@ Proof.
    clear H1.
    intuition.
   intuition.
- intuition.
+ intuition; auto with *.
 Qed.
 
 Lemma lexi_dec:(forall (k i l:nat),
@@ -262,12 +262,12 @@ Proof.
    right.
    unfold Not.
    intro H2.
-   intuition.
+   intuition; auto with *.
   intro H1.
   left.
   right.
   intuition.
- intuition.
+ intuition; auto with *.
 Qed.
 
 
diff --git a/model/structures/Qinf.v b/model/structures/Qinf.v
index 5761eefa..fde1055f 100644
--- a/model/structures/Qinf.v
+++ b/model/structures/Qinf.v
@@ -26,8 +26,8 @@ Instance setoid: Setoid T.
 Proof with intuition.
  constructor.
    intros []...
-  intros [] [] ?...
- intros [x|] [y|] [z|] ??...
+  intros [] [] ?; intuition; auto with *.
+ intros [x|] [y|] [z|] ??; intuition; auto with *.
  change (x = z).
  transitivity y...
 Qed.
@@ -42,7 +42,7 @@ Definition le (x y: T): Prop :=
 #[global]
 Instance: Proper (=) le.
 Proof.
- intros [|] [|] E [|] [|] F; intuition; simpl; try reflexivity.
+ intros [|] [|] E [|] [|] F; intuition; auto with *; simpl; try reflexivity.
  unfold equiv in * |-. simpl in *.
  now rewrite E, F.
 Qed.
diff --git a/model/structures/QnnInf.v b/model/structures/QnnInf.v
index 1699ece1..abd1a09a 100644
--- a/model/structures/QnnInf.v
+++ b/model/structures/QnnInf.v
@@ -17,8 +17,8 @@ Global Instance: Equivalence eq.
 Proof with intuition.
  unfold eq.
  split; repeat intro.
-   destruct x...
-  destruct x, y...
+   destruct x; intuition; auto with *.
+  destruct x, y; intuition; auto with *.
  destruct x, y, z...
  transitivity q0...
 Qed.
@@ -40,7 +40,7 @@ Section liftM2.
   Definition liftM2 (x y: T): T := bind x (fun x' => bind y (fun y' => Finite (f x' y'))).
 
   Global Instance liftM2_Proper: Proper (eq ==> eq ==> eq) liftM2.
-  Proof with intuition. intros [] [] ? [] [] ?... simpl. apply p... Qed.
+  Proof with intuition. intros [] [] ? [] [] ?; intuition; auto with *. simpl. apply p... Qed.
 
   Lemma assoc:
     (forall x y z, f x (f y z) == f (f x y) z)%Qnn ->
diff --git a/model/structures/Qsec.v b/model/structures/Qsec.v
index 149af4cd..13b580f8 100644
--- a/model/structures/Qsec.v
+++ b/model/structures/Qsec.v
@@ -257,7 +257,7 @@ Qed.
 Lemma Qlt_gives_apartness : forall x y : Q, Iff (x/=y) ((x<y) or (y<x)).
 Proof with intuition.
  intros x y; split; intros E.
-  destruct (Q_dec x y)...
+  destruct (Q_dec x y); intuition; auto with *.
  destruct E. 
   apply Qlt_not_eq...
  apply Qnot_eq_sym, Qlt_not_eq...
diff --git a/reals/fast/CRconst.v b/reals/fast/CRconst.v
index 515edda9..6fc7952a 100644
--- a/reals/fast/CRconst.v
+++ b/reals/fast/CRconst.v
@@ -17,7 +17,7 @@ Section const_fun_uc.
 
  Lemma const_uc_prf : is_UniformlyContinuousFunction const_raw const_mu.
  Proof.
-  unfold is_UniformlyContinuousFunction; now intuition.
+  unfold is_UniformlyContinuousFunction; now intuition; auto with *.
  Qed.
 
  (** [const_uc c] defines the uniformly continuous function [λ _, c] *)
diff --git a/reals/fast/CRstreams.v b/reals/fast/CRstreams.v
index 192a90cf..52fbd9f0 100644
--- a/reals/fast/CRstreams.v
+++ b/reals/fast/CRstreams.v
@@ -421,7 +421,7 @@ Proof.
  rewrite nat_of_P_succ_morphism in X.
  rewrite <- plus_n_Sm.
  assert (forall (n m:nat), eq (Z_of_nat n) (Z_of_nat m) -> eq n m).
- { intros i j H. intuition. }
+ { intros i j H. intuition; auto with *. }
  apply H. clear H.
  apply Zmult_reg_l with (Z.of_nat (nat_of_P b));
    [rewrite positive_nat_Z; auto with *|].
diff --git a/stdlib_omissions/List.v b/stdlib_omissions/List.v
index f86401a6..1278f624 100644
--- a/stdlib_omissions/List.v
+++ b/stdlib_omissions/List.v
@@ -70,9 +70,9 @@ Proof with auto.
  apply NoDup_cons.
   intros [?|?]...
   subst y.
-  intuition.
+  intuition; auto with *.
  apply NoDup_cons...
- intuition.
+ intuition; auto with *.
 Qed.
 
 #[global]
diff --git a/stdlib_omissions/Q.v b/stdlib_omissions/Q.v
index 4c731c04..469b5b74 100644
--- a/stdlib_omissions/Q.v
+++ b/stdlib_omissions/Q.v
@@ -118,8 +118,8 @@ Proof with intuition.
  split; intro E.
   setoid_replace x with (x + z - z)%Q by (simpl; ring).
   setoid_replace y with (y + z - z)%Q by (simpl; ring).
-  rewrite E...
- rewrite E...
+  rewrite E; intuition; auto with *.
+ rewrite E; auto with *.
 Qed.
 
 Lemma Qminus_eq (x y: Q): (x - y == 0 <-> x == y)%Q.
@@ -460,7 +460,7 @@ Proof with intuition.
  intros.
  apply Qlt_le_trans with (inject_Z (Z_of_nat n) + 1).
   do 2 rewrite (Qplus_comm (inject_Z (Z_of_nat n))).
-  apply Qplus_lt_l...
+  apply Qplus_lt_l; auto with *.
  pose proof (inj_le _ _ H).
  rewrite Zle_Qle in H0.
  rewrite <- S_Qplus...
diff --git a/util/Qsums.v b/util/Qsums.v
index d50f7ce6..99f3a04f 100644
--- a/util/Qsums.v
+++ b/util/Qsums.v
@@ -153,7 +153,7 @@ Proof with intuition.
    with (e * (1#n)).
   apply Qball_Qabs...
   unfold canonical_names.equiv, stdlib_rationals.Q_eq.
- rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P...
+ rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; intuition; auto with *.
 Qed.
 
 Lemma Qmult_Σ (f: nat -> Q) n (k: nat):
diff --git a/util/SetoidPermutation.v b/util/SetoidPermutation.v
index aade0a2e..3e90498b 100644
--- a/util/SetoidPermutation.v
+++ b/util/SetoidPermutation.v
@@ -20,9 +20,9 @@ Section def.
   Proof with eauto; intuition.
    constructor...
     intro l.
-    induction l...
+    induction l; eauto; intuition; auto with *.
    intros x y H.
-   induction H...
+   induction H; eauto; intuition; auto with *.
   Qed.
 
   Global Instance: Proper (list_eq e ==> list_eq e ==> iff) SetoidPermutation.
@@ -69,7 +69,7 @@ Lemma SetoidPermutation_meaning {A} (R: relation A) `{!Equivalence R} (x y: list
 Proof with auto.
  split.
   intro H. induction H.
-     exists nil. intuition.
+     exists nil. intuition; auto with *.
     destruct IHSetoidPermutation as [?[??]].
     exists (y :: x0).
     repeat split...
@@ -82,7 +82,7 @@ Proof with auto.
   exists x1.
   split.
    transitivity x; intuition.
-  transitivity x0; intuition.
+  transitivity x0; intuition; auto with *.
  intros [?[E?]]. rewrite E.
  symmetry. apply SetoidPermutation_from_Permutation...
  apply _.
@@ -99,11 +99,11 @@ Proof with simpl; auto; try reflexivity.
   apply s_perm_trans with (x y0 :: x x0 :: map y l).
    apply s_perm_skip...
    apply s_perm_skip...
-   induction l... intuition.
+   induction l... intuition; auto with *.
   apply s_perm_trans with (y y0 :: y x0 :: map y l)...
   unfold respectful in *.
-  apply s_perm_skip. intuition.
-  apply s_perm_skip... intuition.
+  apply s_perm_skip. intuition; auto with *.
+  apply s_perm_skip... intuition; auto with *.
  apply s_perm_trans with (map y l')...
  apply s_perm_trans with (map x l')...
  clear IHX1 IHX2 X1 X2.