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

1 files changed, 3 insertions, 3 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.