Merge remote-tracking branch 'github/evarunsafe' into trunk

3 files changed, 8 insertions, 15 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 65123108f..960bdb649 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -363,6 +363,7 @@ let set_norm v = v.norm <- Norm
 let is_val v = match v.norm with Norm -> true | _ -> false
 
 let mk_atom c = {norm=Norm;term=FAtom c}
+let mk_red f = {norm=Red;term=f}
 
 (* Could issue a warning if no is still Red, pointing out that we loose
    sharing. *)
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 07176cb7d..8e172290f 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -164,6 +164,9 @@ val inject : constr -> fconstr
 (** mk_atom: prevents a term from being evaluated *)
 val mk_atom : constr -> fconstr
 
+(** mk_red: makes a reducible term (used in newring) *)
+val mk_red : fterm -> fconstr
+
 val fterm_of : fconstr -> fterm
 val term_of_fconstr : fconstr -> constr
 val destFLambda :
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 7af72b07c..57ef92032 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