eq fusionne avec eqT et devient par défaut sur Type,

idem pour ex et exT, ex2 et exT2, all et allT


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

3 files changed, 12 insertions, 6 deletions

diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index f2fe16f3a1..98b4cb858d 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -138,7 +138,8 @@ Hint SR_plus_zero_right2_T := Resolve (SR_plus_zero_right2 T).
 Hint SR_mult_one_right_T := Resolve (SR_mult_one_right T).
 Hint SR_mult_one_right2_T := Resolve (SR_mult_one_right2 T).
 Hint SR_plus_reg_right_T := Resolve (SR_plus_reg_right T).
-Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Resolve refl_equal sym_equal trans_equal.
+(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hints Immediate T.
 
 Remark iacs_aux_ok : (x:A)(s:abstract_sum)
@@ -445,7 +446,8 @@ Hint Th_plus_zero_right2_T := Resolve (Th_plus_zero_right2 T).
 Hint Th_mult_one_right_T := Resolve (Th_mult_one_right T).
 Hint Th_mult_one_right2_T := Resolve (Th_mult_one_right2 T).
 Hint Th_plus_reg_right_T := Resolve (Th_plus_reg_right T).
-Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Resolve refl_equal sym_equal trans_equal.
+(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hints Immediate T.
 
 Lemma isacs_aux_ok : (x:A)(s:signed_sum)
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 4e6317aced..c146dcc333 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -366,7 +366,8 @@ Hint SR_plus_zero_right2_T := Resolve (SR_plus_zero_right2 T).
 Hint SR_mult_one_right_T := Resolve (SR_mult_one_right T).
 Hint SR_mult_one_right2_T := Resolve (SR_mult_one_right2 T).
 Hint SR_plus_reg_right_T := Resolve (SR_plus_reg_right T).
-Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Resolve refl_equal sym_equal trans_equal.
+(* Hints Resolve refl_eqT sym_eqT trans_eqT. *)
 Hints Immediate T.
 
 Lemma varlist_eq_prop : (x,y:varlist)
@@ -789,7 +790,8 @@ Hint Th_plus_zero_right2_T := Resolve (Th_plus_zero_right2 T).
 Hint Th_mult_one_right_T := Resolve (Th_mult_one_right T).
 Hint Th_mult_one_right2_T := Resolve (Th_mult_one_right2 T).
 Hint Th_plus_reg_right_T := Resolve (Th_plus_reg_right T).
-Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Resolve refl_equal sym_equal trans_equal.
+(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hints Immediate T.
 
 (*** Definitions *)
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 085ff557de..c34c972f79 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -380,7 +380,8 @@ Hint SSR_plus_zero_right2_T := Resolve (SSR_plus_zero_right2 S T).
 Hint SSR_mult_one_right_T := Resolve (SSR_mult_one_right S T).
 Hint SSR_mult_one_right2_T := Resolve (SSR_mult_one_right2 S T).
 Hint SSR_plus_reg_right_T := Resolve (SSR_plus_reg_right S T).
-Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Resolve refl_equal sym_equal trans_equal.
+(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hints Immediate T.
 
 Lemma varlist_eq_prop : (x,y:varlist)
@@ -1036,7 +1037,8 @@ Hint STh_plus_zero_right2_T := Resolve (STh_plus_zero_right2 S T).
 Hint STh_mult_one_right_T := Resolve (STh_mult_one_right S T).
 Hint STh_mult_one_right2_T := Resolve (STh_mult_one_right2 S T).
 Hint STh_plus_reg_right_T := Resolve (STh_plus_reg_right S plus_morph T).
-Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Resolve refl_equal sym_equal trans_equal.
+(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hints Immediate T.