3 files changed, 7 insertions, 18 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 154ec6e1bf..57ef920325 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -34,15 +34,6 @@ open Proofview.Notations
 (****************************************************************************)
 (* controlled reduction *)
 
-(** ppedrot: something dubious here, we're obviously using evars the wrong
-    way. FIXME! *)
-
-let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|])
-let unmark_arg f c =
-  match destEvar c with
-    | (i,[|c|]) -> f (Evar.repr i) c
-    | _ -> assert false
-
 type protect_flag = Eval|Prot|Rec
 
 let tag_arg tag_rec map subs i c =
@@ -75,12 +66,10 @@ and mk_clos_app_but f_map subs f args n =
     let fargs, args' = Array.chop n args in
     let f' = mkApp(f,fargs) in
     match f_map (global_of_constr_nofail f') with
-        Some map ->
-          mk_clos_deep
-            (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s'))
-            subs
-            (mkApp (mark_arg (-1) f', Array.mapi mark_arg args'))
-      | None -> mk_clos_app_but f_map subs f args (n+1)
+    | Some map ->
+       let f i t = tag_arg (mk_clos_but f_map subs) map subs i t in
+       mk_red (FApp (f (-1) f', Array.mapi f args'))
+    | None -> mk_atom (mkApp (f, args))
 
 let interp_map l t =
   try Some(List.assoc_f eq_gr t l) with Not_found -> None
@@ -106,6 +95,7 @@ let protect_tac_in map id =
 (****************************************************************************)
 
 let closed_term t l =
+  let open Quote_plugin in
   let l = List.map Universes.constr_of_global l in
   let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
   if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt())
diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib
deleted file mode 100644
index 7d6c495889..0000000000
--- a/plugins/setoid_ring/newring_plugin.mllib
+++ /dev/null
@@ -1,3 +0,0 @@
-Newring
-Newring_plugin_mod
-G_newring
diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack
new file mode 100644
index 0000000000..23663b4090
--- /dev/null
+++ b/plugins/setoid_ring/newring_plugin.mlpack
@@ -0,0 +1,2 @@
+Newring
+G_newring