Avoid declaring hints about refl/sym/trans of eq in DecidableType2

 This used to be convenient in FSets, but since we now try to integrate
 DecidableType and OrderedType as foundation for other part of the stdlib,
 this should be avoided, otherwise some eauto take a _long_ time.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12626 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 12 insertions, 12 deletions

diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 12cf01cae..5b81cadd2 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -457,7 +457,7 @@ Qed.
 Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a * b) mod n == ((a mod n) * (b mod n)) mod n.
 Proof.
- intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial.
+ intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. reflexivity.
  now destruct (mod_bound b n).
 Qed.
 
@@ -468,7 +468,7 @@ Proof.
  generalize (add_nonneg_nonneg _ _ Ha Hb).
  rewrite (div_mod a n) at 1 2; [|order].
  rewrite <- add_assoc, add_comm, mul_comm.
- intros. rewrite mod_add; trivial.
+ intros. rewrite mod_add; trivial. reflexivity.
  apply add_nonneg_nonneg; auto. destruct (mod_bound a n); auto.
 Qed.
 
@@ -481,7 +481,7 @@ Qed.
 Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a+b) mod n == (a mod n + b mod n) mod n.
 Proof.
- intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial.
+ intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. reflexivity.
  now destruct (mod_bound b n).
 Qed.
 
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 2d627dbc7..6dcc9e91f 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -164,8 +164,8 @@ Hypothesis Initial : initial init.
 Lemma initial_unique : forall m, initial m -> m == init.
 Proof.
 intros m Im. destruct (itersucc_or_itersucc init m) as (p,[H|H]).
-destruct p; simpl in *; auto. destruct (Initial _ H).
-destruct p; simpl in *; auto with *. destruct (Im _ H).
+destruct p. now simpl in *. destruct (Initial _ H).
+destruct p. now simpl in *. destruct (Im _ H).
 Qed.
 
 (** ... then all other points are descendant of it. *)
@@ -287,7 +287,7 @@ Qed.
 
 Lemma ofnat_succ : forall n, [Datatypes.S n] == succ [n].
 Proof.
- unfold ofnat. intros. simpl; auto.
+ now unfold ofnat.
 Qed.
 
 Lemma ofnat_pred : forall n, n<>O -> [Peano.pred n] == P [n].
@@ -336,7 +336,7 @@ Qed.
 
 Lemma ofnat_eq : forall n m, [n]==[m] <-> n = m.
 Proof.
-split. apply ofnat_injective. intros; subst; auto.
+split. apply ofnat_injective. intros; now subst.
 Qed.
 
 (* In addition, we can prove that [ofnat] preserves order. *)
@@ -382,8 +382,8 @@ Qed.
 Lemma ofnat_add : forall n m, [n+m] == [n]+[m].
 Proof.
  intros. rewrite ofnat_add_l.
- induction n; simpl; auto.
- rewrite ofnat_succ. apply succ_wd; auto.
+ induction n; simpl. reflexivity.
+ rewrite ofnat_succ. now apply succ_wd.
 Qed.
 
 Lemma ofnat_mul : forall n m, [n*m] == [n]*[m].
@@ -392,21 +392,21 @@ Proof.
  symmetry. apply mul_0_l.
  rewrite plus_comm.
  rewrite ofnat_succ, ofnat_add, mul_succ_l.
- apply add_wd; auto.
+ now apply add_wd.
 Qed.
 
 Lemma ofnat_sub_r : forall n m, n-[m] == (P^m) n.
 Proof.
  induction m; simpl; intros.
  rewrite ofnat_zero. apply sub_0_r.
- rewrite ofnat_succ, sub_succ_r. apply pred_wd; auto.
+ rewrite ofnat_succ, sub_succ_r. now apply pred_wd.
 Qed.
 
 Lemma ofnat_sub : forall n m, m<=n -> [n-m] == [n]-[m].
 Proof.
  intros n m H. rewrite ofnat_sub_r.
  revert n H. induction m. intros.
- rewrite <- minus_n_O. simpl; auto.
+ rewrite <- minus_n_O. now simpl.
  intros.
  destruct n.
  inversion H.