5 files changed, 13 insertions, 17 deletions
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index 65a397ac..b2e5cc4b 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -1619,6 +1619,7 @@ split.
 generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
 apply H0.
 generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto.
+clear get_sign get_sign_spec. 
 generalize Hp; case l0; simpl; intuition.
 Qed.
 
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index c1fa963f..e664b3b7 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -38,14 +38,6 @@ Proof.
  exact Zmult_plus_distr_l. trivial. exact Zminus_diag.
 Qed.
 
- Lemma Zeqb_ok : forall x y, Zeq_bool x y = true -> x = y.
- Proof.
-  intros x y.
-  assert (H := Zcompare_Eq_eq x y);unfold Zeq_bool;
-  destruct (Zcompare x y);intros H1;auto;discriminate H1.
- Qed.
-
-
 (** Two generic morphisms from Z to (abrbitrary) rings, *)
 (**second one is more convenient for proofs but they are ext. equal*)
 Section ZMORPHISM.
@@ -174,7 +166,7 @@ Section ZMORPHISM.
    Zeq_bool x y = true -> [x] == [y].
  Proof.
   intros x y H.
-  assert (H1 := Zeqb_ok x y H);unfold IDphi in H1.
+  assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1.
   rewrite H1;rrefl.
  Qed.
   
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index 29feab5c..531ab3ca 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -494,7 +494,7 @@ Qed.
  Proof. intros;mrewrite. Qed.
 
  Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y.
- Proof. 
+ Proof.
   intros;mrewrite. 
   repeat rewrite (ARth.(ARmul_comm) z);sreflexivity.
  Qed.
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index 4a5b623b..942915ab 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -50,7 +50,7 @@ Ltac Zpower_neg :=
   end.   
 
 Add Ring Zr : Zth
-  (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
+  (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
    power_tac Zpower_theory [Zpow_tac],
     (* The two following option are not needed, it is the default chose when the set of 
         coefficiant is usual ring Z *)
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index dd79801d..3d022add 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(*i $Id: newring.ml4 11094 2008-06-10 19:35:23Z herbelin $ i*)
+(*i $Id: newring.ml4 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 open Pp
 open Util
@@ -452,11 +452,14 @@ let (theory_to_obj, obj_to_theory) =
 
 
 let setoid_of_relation env a r =
-  lapp coq_mk_Setoid
-    [|a ; r ; 
-      Class_tactics.reflexive_proof env a r ; 
-      Class_tactics.symmetric_proof env a r ; 
-      Class_tactics.transitive_proof env a r |]
+  try 
+    lapp coq_mk_Setoid
+      [|a ; r ; 
+	Class_tactics.reflexive_proof env a r ; 
+	Class_tactics.symmetric_proof env a r ; 
+	Class_tactics.transitive_proof env a r |]
+  with Not_found ->
+    error "cannot find setoid relation"
 
 let op_morph r add mul opp req m1 m2 m3 =
   lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |]