3 files changed, 6 insertions, 7 deletions
diff --git a/contrib/setoid_ring/Ring_base.v b/contrib/setoid_ring/Ring_base.v
index 95b037e3..956a15fe 100644
--- a/contrib/setoid_ring/Ring_base.v
+++ b/contrib/setoid_ring/Ring_base.v
@@ -10,7 +10,6 @@
    ring tactic. Abstract rings need more theory, depending on
    ZArith_base. *)
 
-Declare ML Module "newring".
 Require Export Ring_theory.
 Require Export Ring_tac.
 Require Import InitialRing.
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 46d106d3..ad20fa08 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -4,7 +4,6 @@ Require Import BinPos.
 Require Import Ring_polynom.
 Require Import BinList.
 Require Import InitialRing.
-Declare ML Module "newring".
   
 
 (* adds a definition id' on the normal form of t and an hypothesis id
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 3d022add..50b7e47b 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 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: newring.ml4 11800 2009-01-18 18:34:15Z msozeau $ i*)
 
 open Pp
 open Util
@@ -19,12 +19,12 @@ open Environ
 open Libnames
 open Tactics
 open Rawterm
+open Termops
 open Tacticals
 open Tacexpr
 open Pcoq
 open Tactic
 open Constr
-open Setoid_replace
 open Proof_type
 open Coqlib
 open Tacmach
@@ -452,12 +452,13 @@ let (theory_to_obj, obj_to_theory) =
 
 
 let setoid_of_relation env a r =
+  let evm = Evd.empty in
   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 |]
+	Class_tactics.get_reflexive_proof env evm a r ; 
+	Class_tactics.get_symmetric_proof env evm a r ; 
+	Class_tactics.get_transitive_proof env evm a r |]
   with Not_found ->
     error "cannot find setoid relation"