5 files changed, 20 insertions, 35 deletions
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 05ab8ab326..ada41274fa 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+open Grammar_API
 open Ltac_plugin
 open Pp
 open Util
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 38f05978db..ee75d2908e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Ltac_plugin
 open Pp
 open Util
@@ -47,7 +48,7 @@ let tag_arg tag_rec map subs i c =
 let global_head_of_constr sigma c = 
   let f, args = decompose_app sigma c in
     try fst (Termops.global_of_constr sigma f)
-    with Not_found -> CErrors.anomaly (str "global_head_of_constr")
+    with Not_found -> CErrors.anomaly (str "global_head_of_constr.")
 
 let global_of_constr_nofail c = 
   try global_of_constr c
@@ -151,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) 
@@ -282,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 ;;
@@ -346,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"
@@ -749,7 +754,7 @@ let ltac_ring_structure e =
    lemma1;lemma2;pretac;posttac]
 
 let ring_lookup (f : Value.t) lH rl t =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     try (* find_ring_strucure can raise an exception *)
@@ -761,7 +766,7 @@ let ring_lookup (f : Value.t) lH rl t =
       let ring = ltac_ring_structure e in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  end }
+  end
 
 (***********************************************************************)
 
@@ -769,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"
@@ -929,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
@@ -1035,7 +1040,7 @@ let ltac_field_structure e =
    field_simpl_eq_in_ok;cond_ok;pretac;posttac]
 
 let field_lookup (f : Value.t) lH rl t =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     try
@@ -1047,4 +1052,4 @@ let field_lookup (f : Value.t) lH rl t =
       let field = ltac_field_structure e in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  end }
+  end
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index d9d32c681d..7f685063c4 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open EConstr
 open Libnames
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
index c26fcc8d1f..b7afd2effc 100644
--- a/plugins/setoid_ring/newring_ast.mli
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Constr
+open API
+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