3 files changed, 10 insertions, 30 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index a107b59482..ee75d2908e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -152,7 +152,7 @@ let ic_unsafe c = (*FIXME remove *)
     EConstr.of_constr (fst (Constrintern.interp_constr env sigma c))
 
 let decl_constant na ctx c =
-  let open Constr in
+  let open Term in
   let vars = Universes.universes_of_constr c in
   let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
   mkConst(declare_constant (Id.of_string na) 
@@ -283,7 +283,7 @@ let my_reference c =
 let znew_ring_path =
   DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
-  lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s))
+  lazy(KerName.make (ModPath.MPfile znew_ring_path) DirPath.empty (Label.make s))
 
 let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);;
 let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
@@ -347,7 +347,11 @@ let _ = add_map "ring"
 
 let pr_constr c = pr_econstr c
 
-module Cmap = Map.Make(Constr)
+module M = struct
+  type t = Term.constr
+  let compare = Term.compare
+end
+module Cmap = Map.Make(M)
 
 let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
 let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table"
@@ -770,7 +774,7 @@ let new_field_path =
   DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
 
 let field_ltac s =
-  lazy(make_kn (MPfile new_field_path) DirPath.empty (Label.make s))
+  lazy(KerName.make (ModPath.MPfile new_field_path) DirPath.empty (Label.make s))
 
 
 let _ = add_map "field"
@@ -930,7 +934,7 @@ let field_equality evd r inv req =
 	  inv_m_lem
 
 let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
-  let open Constr in
+  let open Term in
   check_required_library (cdir@["Field_tac"]);
   let (sigma,fth) = ic fth in
   let env = Global.env() in
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
index 46572acd0f..b7afd2effc 100644
--- a/plugins/setoid_ring/newring_ast.mli
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open API
-open Constr
+open Term
 open Libnames
 open Constrexpr
 open Tacexpr
diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget
deleted file mode 100644
index 595ba55ec6..0000000000
--- a/plugins/setoid_ring/vo.itarget
+++ /dev/null
@@ -1,24 +0,0 @@
-ArithRing.vo
-BinList.vo
-Field_tac.vo
-Field_theory.vo
-Field.vo
-InitialRing.vo
-NArithRing.vo
-RealField.vo
-Ring_base.vo
-Ring_polynom.vo
-Ring_tac.vo
-Ring_theory.vo
-Ring.vo
-ZArithRing.vo
-Algebra_syntax.vo
-Cring.vo
-Ncring.vo
-Ncring_polynom.vo
-Ncring_initial.vo
-Ncring_tac.vo
-Rings_Z.vo
-Rings_R.vo
-Rings_Q.vo
-Integral_domain.vo
-\ No newline at end of file