Reductionops now return EConstrs.

12 files changed, 54 insertions, 39 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 93bd88fe4..a0b04ce3b 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -182,6 +182,7 @@ module Btauto = struct
     let var = EConstr.of_constr var in
     (* Compute an assignment that dissatisfies the goal *)
     let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in
+    let var = EConstr.Unsafe.to_constr var in
     let rec to_list l = match decomp_term (Tacmach.project gl) l with
     | Term.App (c, _)
       when c === (Lazy.force CoqList._nil) -> []
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c3254010a..7123ebcaf 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1103,7 +1103,7 @@ let thesis_for obj typ per_info env=
       ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
 	 str "cannot give an induction hypothesis (wrong parameters).") in
   let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
-    compose_prod rc (Reductionops.whd_beta Evd.empty (EConstr.of_constr hd2))
+    compose_prod rc (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty (EConstr.of_constr hd2)))
 
 let rec build_product_dep pat_info per_info args body gls =
   match args with
@@ -1233,7 +1233,7 @@ let hrec_for fix_id per_info gls obj_id =
     try List.for_all2 Term.eq_constr params per_info.per_params with
         Invalid_argument _ -> false end;
   let hd2 = applist (mkVar fix_id,args@[obj]) in
-    EConstr.of_constr (compose_lam rc (Reductionops.whd_beta gls.sigma (EConstr.of_constr hd2)))
+    EConstr.of_constr (compose_lam rc (EConstr.Unsafe.to_constr (Reductionops.whd_beta gls.sigma (EConstr.of_constr hd2))))
 
 let warn_missing_case =
   CWarnings.create ~name:"declmode-missing-case" ~category:"declmode"
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 460157130..61547f96d 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -70,11 +70,17 @@ type scheme = TypeScheme | Default
 
 type flag = info * scheme
 
+let whd_all env t =
+  EConstr.Unsafe.to_constr (whd_all env none (EConstr.of_constr t))
+
+let whd_betaiotazeta t =
+  EConstr.Unsafe.to_constr (whd_betaiotazeta none (EConstr.of_constr t))
+
 (*s [flag_of_type] transforms a type [t] into a [flag].
   Really important function. *)
 
 let rec flag_of_type env t : flag =
-  let t = whd_all env none (EConstr.of_constr t) in
+  let t = whd_all env t in
   match kind_of_term t with
     | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
     | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
@@ -105,14 +111,14 @@ let push_rel_assum (n, t) env =
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
 let rec type_sign env c =
-  match kind_of_term (whd_all env none (EConstr.of_constr c)) with
+  match kind_of_term (whd_all env c) with
     | Prod (n,t,d) ->
 	(if is_info_scheme env t then Keep else Kill Kprop)
 	:: (type_sign (push_rel_assum (n,t) env) d)
     | _ -> []
 
 let rec type_scheme_nb_args env c =
-  match kind_of_term (whd_all env none (EConstr.of_constr c)) with
+  match kind_of_term (whd_all env c) with
     | Prod (n,t,d) ->
 	let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in
 	if is_info_scheme env t then n+1 else n
@@ -138,7 +144,7 @@ let make_typvar n vl =
   next_ident_away id' vl
 
 let rec type_sign_vl env c =
-  match kind_of_term (whd_all env none (EConstr.of_constr c)) with
+  match kind_of_term (whd_all env c) with
     | Prod (n,t,d) ->
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
 	if not (is_info_scheme env t) then Kill Kprop::s, vl
@@ -146,7 +152,7 @@ let rec type_sign_vl env c =
     | _ -> [],[]
 
 let rec nb_default_params env c =
-  match kind_of_term (whd_all env none (EConstr.of_constr c)) with
+  match kind_of_term (whd_all env c) with
     | Prod (n,t,d) ->
 	let n = nb_default_params (push_rel_assum (n,t) env) d in
 	if is_default env t then n+1 else n
@@ -217,7 +223,7 @@ let parse_ind_args si args relmax =
 
 
 let rec extract_type env db j c args =
-  match kind_of_term (whd_betaiotazeta none (EConstr.of_constr c)) with
+  match kind_of_term (whd_betaiotazeta c) with
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
 	extract_type env db j d (Array.to_list args' @ args)
@@ -319,7 +325,7 @@ and extract_type_app env db (r,s) args =
 and extract_type_scheme env db c p =
   if Int.equal p 0 then extract_type env db 0 c []
   else
-    let c = whd_betaiotazeta none (EConstr.of_constr c) in
+    let c = whd_betaiotazeta c in
     match kind_of_term c with
       | Lambda (n,t,d) ->
           extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
@@ -492,7 +498,7 @@ and extract_really_ind env kn mib =
 *)
 
 and extract_type_cons env db dbmap c i =
-  match kind_of_term (whd_all env none (EConstr.of_constr c)) with
+  match kind_of_term (whd_all env c) with
     | Prod (n,t,d) ->
 	let env' = push_rel_assum (n,t) env in
 	let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a320b47aa..24d4346d9 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t=
       let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
-      let (nam,_,_)=destProd (whd_all env evmap (EConstr.of_constr typ)) in
+      let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap (EConstr.of_constr typ))) in
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 205cb282d..5520c7e35 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -42,8 +42,8 @@ let unif t1 t2=
     Queue.add (t1,t2) bige;
     try while true do
       let t1,t2=Queue.take bige in
-      let nt1=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t1))
-      and nt2=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t2)) in
+      let nt1=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t1)))
+      and nt2=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t2))) in
 	match (kind_of_term nt1),(kind_of_term nt2) with
 	    Meta i,Meta j->
 	      if not (Int.equal i j) then
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 2e3992be9..188368082 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -321,6 +321,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
     in
     let new_type_of_hyp =
       Reductionops.nf_betaiota Evd.empty (EConstr.of_constr new_type_of_hyp) in
+    let new_type_of_hyp = EConstr.Unsafe.to_constr new_type_of_hyp in
     let new_ctxt,new_end_of_type =
       decompose_prod_n_assum ctxt_size new_type_of_hyp
     in
@@ -619,6 +620,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 		   )
 	 in
 	 let new_body = pf_nf_betaiota g' (EConstr.of_constr (mkApp(fun_body,[| new_term_value |]))) in
+	 let new_body = EConstr.Unsafe.to_constr new_body in
 	 let new_infos =
 	   {dyn_infos with
 	      info = new_body;
@@ -752,6 +754,7 @@ let build_proof
 			     pf_nf_betaiota g'
 			       (EConstr.of_constr (mkApp(dyn_infos.info,[|mkVar id|])))
 			   in
+			   let new_term = EConstr.Unsafe.to_constr new_term in
 			   let new_infos = {dyn_infos with info = new_term} in
 			   let do_prove new_hyps =
 			     build_proof do_finalize
@@ -796,6 +799,7 @@ let build_proof
 		  | Lambda _ ->
 		      let new_term =
                         Reductionops.nf_beta Evd.empty (EConstr.of_constr dyn_infos.info) in
+                      let new_term = EConstr.Unsafe.to_constr new_term in
 		      build_proof do_finalize {dyn_infos with info = new_term}
 			g
 		  | LetIn _ ->
@@ -1097,11 +1101,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
     let get_body const =
       match Global.body_of_constant const with
 	| Some body ->
-	     Tacred.cbv_norm_flags
+	     EConstr.Unsafe.to_constr (Tacred.cbv_norm_flags
 	       (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	       (Global.env ())
 	       (Evd.empty)
-	       (EConstr.of_constr body)
+	       (EConstr.of_constr body))
 	| None -> error ( "Cannot define a principle over an axiom ")
     in
     let fbody = get_body fnames.(fun_num) in
@@ -1152,9 +1156,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    let bodies_with_all_params =
 	      Array.map
 		(fun body ->
-		   Reductionops.nf_betaiota Evd.empty
+		   EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty
 		     (EConstr.of_constr (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
-			      List.rev_map var_of_decl princ_params)))
+			      List.rev_map var_of_decl princ_params))))
 		)
 		bodies
 	    in
@@ -1190,12 +1194,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		   let body_with_param,num =
 		     let body = get_body fnames.(i) in
 		     let body_with_full_params =
-		       Reductionops.nf_betaiota Evd.empty (EConstr.of_constr (
-			 applist(body,List.rev_map var_of_decl full_params)))
+		       EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty (EConstr.of_constr (
+			 applist(body,List.rev_map var_of_decl full_params))))
 		     in
 		     match kind_of_term body_with_full_params with
 		       | Fix((_,num),(_,_,bs)) ->
-			       Reductionops.nf_betaiota Evd.empty
+			       EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty
 				 (EConstr.of_constr (
 				   (applist
 				      (substl
@@ -1203,7 +1207,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 					    (Array.to_list all_funs_with_full_params))
 					 bs.(num),
 				       List.rev_map var_of_decl princ_params))
-				 )),num
+				 ))),num
 			 | _ -> error "Not a mutual block"
 		   in
 		   let info =
@@ -1279,8 +1283,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info =
-		       Reductionops.nf_betaiota Evd.empty
-			 (EConstr.of_constr (applist(fix_body,List.rev_map mkVar args_id)));
+		       EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty
+			 (EConstr.of_constr (applist(fix_body,List.rev_map mkVar args_id))));
 		     eq_hyps = []
 		   }
 		 in
@@ -1339,11 +1343,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info =
-		       Reductionops.nf_betaiota Evd.empty
+		       EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty
 			 (EConstr.of_constr (applist(fbody_with_full_params,
 				  (List.rev_map var_of_decl princ_params)@
 				    (List.rev_map mkVar args_id)
-				 )));
+				 ))));
 		     eq_hyps = []
 		   }
 		 in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 4d88f9f91..b4eb77870 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -409,6 +409,7 @@ let get_funs_constant mp dp =
 	      (Evd.from_env (Global.env ()))
 	      (EConstr.of_constr body)
 	    in
+	    let body = EConstr.Unsafe.to_constr body in
 	    body
 	| None -> error ( "Cannot define a principle over an axiom ")
     in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d29d4694f..c02b64c1f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -252,7 +252,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     (* and the principle to use in this lemma in $\zeta$ normal form *)
     let f_principle,princ_type = schemes.(i) in
     let princ_type =  nf_zeta (EConstr.of_constr princ_type) in
-    let princ_type = EConstr.of_constr princ_type in
     let princ_infos = Tactics.compute_elim_sig evd princ_type in
     (* The number of args of the function is then easily computable *)
     let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
@@ -429,7 +428,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) decl p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
-	     (nf_zeta (EConstr.of_constr p))::bindings,id::avoid)
+	     (EConstr.Unsafe.to_constr (nf_zeta (EConstr.of_constr p)))::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))
@@ -662,7 +661,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     (* We get the constant and the principle corresponding to this lemma *)
     let f = funcs.(i) in
     let graph_principle = nf_zeta (EConstr.of_constr schemes.(i))  in
-    let princ_type = pf_unsafe_type_of g (EConstr.of_constr graph_principle) in
+    let princ_type = pf_unsafe_type_of g graph_principle in
     let princ_type = EConstr.of_constr princ_type in
     let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
     (* Then we get the number of argument of the function
@@ -754,14 +753,15 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	g
     in
     let params_names = fst (List.chop princ_infos.nparams args_names) in
+    let open EConstr in
     let params = List.map mkVar params_names in
     tclTHENSEQ
       [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
 	observe_tac "h_generalize"
-	(Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas))]));
+	(Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
 	Proofview.V82.of_tactic (Simple.intro graph_principle_id);
 	observe_tac "" (tclTHEN_i
-	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (EConstr.mkVar hres,NoBindings) (Some (EConstr.mkVar graph_principle_id,NoBindings)))))
+	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
 	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
@@ -796,6 +796,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
 	 let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in 
 	   let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
+	   let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
 	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
 	)
@@ -863,6 +864,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	   Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
 	 in
 	 let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
+	 let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
 	 observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
 	 type_of_lemma,type_info
 	)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5cee3cb20..c71174fef 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -695,7 +695,7 @@ let mkDestructEq :
         let changefun patvars = { run = fun sigma ->
           let redfun = pattern_occs [Locus.AllOccurrencesBut [1], EConstr.of_constr expr] in
           let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2)) in
-          Sigma (EConstr.of_constr c, sigma, p)
+          Sigma (c, sigma, p)
         } in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
       Proofview.V82.of_tactic (simplest_case (EConstr.of_constr expr))]), to_revert
@@ -1503,6 +1503,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let res_vars,eq' = decompose_prod equation_lemma_type in
   let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in
   let eq' = nf_zeta env_eq' (EConstr.of_constr eq') in
+  let eq' = EConstr.Unsafe.to_constr eq' in
   let res =
 (*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
 (*     Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 72290e681..51790f4c9 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -568,7 +568,7 @@ let abstract_path typ path t =
   mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur
 
 let focused_simpl path gl =
-  let newc = context (fun i t -> pf_nf gl (EConstr.of_constr t)) (List.rev path) (pf_concl gl) in
+  let newc = context (fun i t -> EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr t))) (List.rev path) (pf_concl gl) in
   let newc = EConstr.of_constr newc in
   Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
 
@@ -1386,7 +1386,7 @@ let destructure_omega gl tac_def (id,c) =
   else
     try match destructurate_prop c with
       | Kapp(Eq,[typ;t1;t2])
-	when begin match destructurate_type (pf_nf gl (EConstr.of_constr typ)) with Kapp(Z,[]) -> true | _ -> false end ->
+	when begin match destructurate_type (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) with Kapp(Z,[]) -> true | _ -> false end ->
 	  let t = mk_plus t1 (mk_inv t2) in
 	  normalize_equation
 	    id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
@@ -1661,7 +1661,7 @@ let rec decidability gl t =
     | Kapp(Not,[t1]) ->
         mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |])
     | Kapp(Eq,[typ;t1;t2]) ->
-	begin match destructurate_type (pf_nf gl (EConstr.of_constr typ)) with
+	begin match destructurate_type (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) with
           | Kapp(Z,[]) ->  mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
           | Kapp(Nat,[]) ->  mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
           | _ -> raise Undecidable
@@ -1791,7 +1791,7 @@ let destructure_hyps =
 		   with Not_found -> loop lit)
 	      | Kapp(Eq,[typ;t1;t2]) ->
                   if !old_style_flag then begin
-		    match destructurate_type (pf_nf (EConstr.of_constr typ)) with
+		    match destructurate_type (EConstr.Unsafe.to_constr (pf_nf (EConstr.of_constr typ))) with
 		    | Kapp(Nat,_) ->
                         Tacticals.New.tclTHENLIST [
 			  (simplest_elim
@@ -1808,7 +1808,7 @@ let destructure_hyps =
                         ]
 		    | _ -> loop lit
                   end else begin
-		    match destructurate_type (pf_nf (EConstr.of_constr typ)) with
+		    match destructurate_type (EConstr.Unsafe.to_constr (pf_nf (EConstr.of_constr typ))) with
 		    | Kapp(Nat,_) ->
                         (Tacticals.New.tclTHEN
 			   (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index f2d91bad3..5c68078d7 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -353,7 +353,7 @@ let parse_term t =
 let parse_rel gl t =
   try match destructurate t with
     | Kapp("eq",[typ;t1;t2])
-      when destructurate (Tacmach.pf_nf gl (EConstr.of_constr typ)) = Kapp("Z",[]) -> Req (t1,t2)
+      when destructurate (EConstr.Unsafe.to_constr (Tacmach.pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2)
     | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
     | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2)
     | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 4492b854b..b720b2e0a 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -83,8 +83,8 @@ let lookup_map map =
 
 let protect_red map env sigma c =
   let c = EConstr.Unsafe.to_constr c in
-  kl (create_clos_infos all env)
-    (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);;
+  EConstr.of_constr (kl (create_clos_infos all env)
+    (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c));;
 
 let protect_tac map =
   Tactics.reduct_option (protect_red map,DEFAULTcast) None