2 files changed, 5 insertions, 14 deletions
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 13cf8330b5..b1882ae8ac 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -30,7 +30,7 @@ END
 
 TACTIC EXTEND closed_term
   [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
-    [ closed_term (EConstr.of_constr t) l ]
+    [ closed_term t l ]
 END
 
 open Pptactic
@@ -90,11 +90,7 @@ END
 
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
-    [
-      let lH = List.map EConstr.of_constr lH in
-      let lrt = List.map EConstr.of_constr lrt in
-      let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t
-    ]
+    [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t ]
 END
 
 let pr_field_mod = function
@@ -129,9 +125,5 @@ END
 
 TACTIC EXTEND field_lookup
 | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
-      [
-        let lH = List.map EConstr.of_constr lH in
-        let lt = List.map EConstr.of_constr lt in
-        let (t,l) = List.sep_last lt in field_lookup f lH l t
-      ]
+      [ let (t,l) = List.sep_last lt in field_lookup f lH l t ]
 END
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index c0eeff8d78..ce2c558aeb 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -183,7 +183,7 @@ let dummy_goal env sigma =
   {Evd.it = gl; Evd.sigma = sigma}
 
 let constr_of v = match Value.to_constr v with
-  | Some c -> c
+  | Some c -> EConstr.Unsafe.to_constr c
   | None -> failwith "Ring.exec_tactic: anomaly"
 
 let tactic_res = ref [||]
@@ -203,7 +203,6 @@ let get_res =
 
 let exec_tactic env evd n f args =
   let fold arg (i, vars, lfun) =
-    let arg = EConstr.Unsafe.to_constr arg in
     let id = Id.of_string ("x" ^ string_of_int i) in
     let x = Reference (ArgVar (Loc.ghost, id)) in
     (succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun)
@@ -730,7 +729,7 @@ let make_term_list env evd carrier rl =
     (plapp evd coq_nil [|carrier|])
   in Typing.e_solve_evars env evd l
 
-let carg = Tacinterp.Value.of_constr
+let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c)
 let tacarg expr =
   Tacinterp.Value.of_closure (Tacinterp.default_ist ()) expr