Reductionops API using EConstr.

15 files changed, 53 insertions, 50 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 46fa5b408..c17c8dbb8 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1092,7 +1092,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 hd2)
+    compose_prod rc (Reductionops.whd_beta Evd.empty (EConstr.of_constr hd2))
 
 let rec build_product_dep pat_info per_info args body gls =
   match args with
@@ -1222,7 +1222,7 @@ let hrec_for fix_id per_info gls obj_id =
     try List.for_all2 eq_constr params per_info.per_params with
         Invalid_argument _ -> false end;
   let hd2 = applist (mkVar fix_id,args@[obj]) in
-    compose_lam rc (Reductionops.whd_beta gls.sigma hd2)
+    compose_lam rc (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 85cacecdb..6ca34036a 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -74,7 +74,7 @@ type flag = info * scheme
   Really important function. *)
 
 let rec flag_of_type env t : flag =
-  let t = whd_all env none t in
+  let t = whd_all env none (EConstr.of_constr 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)
@@ -102,14 +102,14 @@ let is_info_scheme env t = match flag_of_type env t with
 (*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 c) with
+  match kind_of_term (whd_all env none (EConstr.of_constr 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 c) with
+  match kind_of_term (whd_all env none (EConstr.of_constr 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
@@ -135,7 +135,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 c) with
+  match kind_of_term (whd_all env none (EConstr.of_constr 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
@@ -143,7 +143,7 @@ let rec type_sign_vl env c =
     | _ -> [],[]
 
 let rec nb_default_params env c =
-  match kind_of_term (whd_all env none c) with
+  match kind_of_term (whd_all env none (EConstr.of_constr 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
@@ -214,7 +214,7 @@ let parse_ind_args si args relmax =
 
 
 let rec extract_type env db j c args =
-  match kind_of_term (whd_betaiotazeta Evd.empty c) with
+  match kind_of_term (whd_betaiotazeta none (EConstr.of_constr c)) with
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
 	extract_type env db j d (Array.to_list args' @ args)
@@ -297,7 +297,7 @@ and extract_type_app env db (r,s) args =
   let ml_args =
     List.fold_right
       (fun (b,c) a -> if b == Keep then
-	 let p = List.length (fst (splay_prod env none (type_of env c))) in
+	 let p = List.length (fst (splay_prod env none (EConstr.of_constr (type_of env c)))) in
          let db = iterate (fun l -> 0 :: l) p db in
          (extract_type_scheme env db c p) :: a
        else a)
@@ -316,12 +316,12 @@ 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 Evd.empty c in
+    let c = whd_betaiotazeta none (EConstr.of_constr 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)
       | _ ->
-          let rels = fst (splay_prod env none (type_of env c)) in
+          let rels = fst (splay_prod env none (EConstr.of_constr (type_of env c))) in
           let env = push_rels_assum rels env in
           let eta_args = List.rev_map mkRel (List.interval 1 p) in
           extract_type env db 0 (lift p c) eta_args
@@ -488,7 +488,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 c) with
+  match kind_of_term (whd_all env none (EConstr.of_constr 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
@@ -846,7 +846,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
    and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
 
 let decomp_lams_eta_n n m env c t =
-  let rels = fst (splay_prod_n env none n t) in
+  let rels = fst (splay_prod_n env none n (EConstr.of_constr t)) in
   let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in
   let rels',c = decompose_lam c in
   let d = n - m in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index eebd974ea..a3513692c 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 idc in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
-      let (nam,_,_)=destProd (whd_all env evmap typ) in
+      let (nam,_,_)=destProd (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 01c019744..fb237f29b 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -41,8 +41,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 t1)
-      and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) 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
 	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 f6567ab81..258ee5ad6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -318,7 +318,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	context
     in
     let new_type_of_hyp =
-      Reductionops.nf_betaiota Evd.empty new_type_of_hyp in
+      Reductionops.nf_betaiota Evd.empty (EConstr.of_constr new_type_of_hyp) in
     let new_ctxt,new_end_of_type =
       decompose_prod_n_assum ctxt_size new_type_of_hyp
     in
@@ -786,7 +786,7 @@ let build_proof
 		      do_finalize dyn_infos  g
 		  | Lambda _ ->
 		      let new_term =
-                        Reductionops.nf_beta Evd.empty dyn_infos.info in
+                        Reductionops.nf_beta Evd.empty (EConstr.of_constr dyn_infos.info) in
 		      build_proof do_finalize {dyn_infos with info = new_term}
 			g
 		  | LetIn _ ->
@@ -1090,7 +1090,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	       (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	       (Global.env ())
 	       (Evd.empty)
-	       body
+	       (EConstr.of_constr body)
 	| None -> error ( "Cannot define a principle over an axiom ")
     in
     let fbody = get_body fnames.(fun_num) in
@@ -1142,8 +1142,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	      Array.map
 		(fun body ->
 		   Reductionops.nf_betaiota Evd.empty
-		     (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
-			      List.rev_map var_of_decl princ_params))
+		     (EConstr.of_constr (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
+			      List.rev_map var_of_decl princ_params)))
 		)
 		bodies
 	    in
@@ -1179,20 +1179,20 @@ 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 (
-			 applist(body,List.rev_map var_of_decl full_params))
+		       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.of_constr (
 				   (applist
 				      (substl
 					 (List.rev
 					    (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 =
@@ -1269,7 +1269,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     rec_hyps = [];
 		     info =
 		       Reductionops.nf_betaiota Evd.empty
-			 (applist(fix_body,List.rev_map mkVar args_id));
+			 (EConstr.of_constr (applist(fix_body,List.rev_map mkVar args_id)));
 		     eq_hyps = []
 		   }
 		 in
@@ -1329,10 +1329,10 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     rec_hyps = [];
 		     info =
 		       Reductionops.nf_betaiota Evd.empty
-			 (applist(fbody_with_full_params,
+			 (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 032d887de..9637632a6 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -405,7 +405,7 @@ let get_funs_constant mp dp =
 	      (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	      (Global.env ())
 	      (Evd.from_env (Global.env ()))
-	      body
+	      (EConstr.of_constr body)
 	    in
 	    body
 	| None -> error ( "Cannot define a principle over an axiom ")
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index de2e5ea4e..92de4d873 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -352,7 +352,7 @@ let add_pat_variables pat typ env : Environ.env =
       | PatVar(_,na) -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
       | PatCstr(_,c,patl,na) ->
 	  let Inductiveops.IndType(indf,indargs) =
-	    try Inductiveops.find_rectype env (Evd.from_env env) typ
+	    try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
 	    with Not_found -> assert false
 	  in
 	  let constructors = Inductiveops.get_constructors env indf in
@@ -409,7 +409,7 @@ let rec pattern_to_term_and_type env typ  = function
 	  constr
       in
       let Inductiveops.IndType(indf,indargs) =
-	try Inductiveops.find_rectype env (Evd.from_env env) typ
+	try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
 	with Not_found -> assert false
       in
       let constructors = Inductiveops.get_constructors env indf in
@@ -629,7 +629,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
 	let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
 	let (ind,_) =
-	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
+	  try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ)
 	  with Not_found ->
 	    user_err  (str "Cannot find the inductive associated to " ++
 			       Printer.pr_glob_constr b ++ str " in " ++
@@ -661,7 +661,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	  let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
 	  let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
 	  let (ind,_) =
-	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
+	    try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ)
 	    with Not_found ->
 	      user_err  (str "Cannot find the inductive associated to " ++
 				 Printer.pr_glob_constr b ++ str " in " ++
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index cf42a809d..9abe60402 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -251,7 +251,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     let mib,_ = Global.lookup_inductive graph_ind in
     (* 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 princ_type in
+    let princ_type =  nf_zeta (EConstr.of_constr princ_type) in
     let princ_infos = Tactics.compute_elim_sig 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
@@ -428,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 p)::bindings,id::avoid)
+	     (nf_zeta (EConstr.of_constr p))::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))
@@ -496,7 +496,7 @@ and intros_with_rewrite_aux : tactic =
 	      begin
 		match kind_of_term t with
 		  | App(eq,args) when (eq_constr eq eq_ind)  ->
- 		      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
+ 		      if Reductionops.is_conv (pf_env g) (project g) (EConstr.of_constr args.(1)) (EConstr.of_constr args.(2))
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
@@ -655,12 +655,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     *)
     let lemmas =
       Array.map
-	(fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn concl ctxt))
+	(fun (_,(ctxt,concl)) -> nf_zeta (EConstr.of_constr (Termops.it_mkLambda_or_LetIn concl ctxt)))
 	lemmas_types_infos
     in
     (* We get the constant and the principle corresponding to this lemma *)
     let f = funcs.(i) in
-    let graph_principle = nf_zeta schemes.(i)  in
+    let graph_principle = nf_zeta (EConstr.of_constr schemes.(i))  in
     let princ_type = pf_unsafe_type_of g graph_principle in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* Then we get the number of argument of the function
@@ -793,7 +793,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 graphs_constr.(i) <- graph;
 	 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 type_of_lemma in 
-	   let type_of_lemma = nf_zeta type_of_lemma in
+	   let type_of_lemma = nf_zeta (EConstr.of_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
 	)
@@ -860,7 +860,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 type_of_lemma = nf_zeta type_of_lemma in
+	 let type_of_lemma = nf_zeta (EConstr.of_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/merge.ml b/plugins/funind/merge.ml
index 865042afb..222c0c804 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -135,7 +135,7 @@ let prNamedRLDecl s lc =
 
 let showind (id:Id.t) =
   let cstrid = Constrintern.global_reference id in
-  let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
+  let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in
   let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in
   List.iter (fun decl ->
     print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6b63d7771..4fd9e0ff8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -693,7 +693,7 @@ let mkDestructEq :
       (fun g2 ->
         let changefun patvars = { run = fun sigma ->
           let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
-          redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2)
+          redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2))
         } in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
@@ -1499,7 +1499,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
  (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
   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' eq'  in
+  let eq' = nf_zeta env_eq' (EConstr.of_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/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 49fcf83b4..9fb1463db 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -902,7 +902,7 @@ struct
 
 
   let is_convertible gl t1 t2 = 
-   Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) t1 t2
+   Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) (EConstr.of_constr t1) (EConstr.of_constr t2)
 
   let parse_zop gl (op,args) =
    match kind_of_term op with
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 1afc6500b..d15449aef 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1591,7 +1591,7 @@ let nat_inject =
 		  (loop lit)
                 ]
             | Kapp(Eq,[typ;t1;t2]) ->
-		if is_conv typ (Lazy.force coq_nat) then
+		if is_conv (EConstr.of_constr typ) (EConstr.of_constr (Lazy.force coq_nat)) then
                   Tacticals.New.tclTHENLIST [
 		    (generalize_tac
 		      [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index c6376727a..afc7e6665 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -249,8 +249,8 @@ let compute_ivs f cs gl =
            (* Then we test if the RHS is the RHS for variables *)
                    else begin match decompose_app bodyi with
                      | vmf, [_; _; a3; a4 ]
-                         when isRel a3 && isRel a4 && is_conv vmf
-                           (Lazy.force coq_varmap_find)->
+                         when isRel a3 && isRel a4 && is_conv (EConstr.of_constr vmf)
+                           (EConstr.of_constr (Lazy.force coq_varmap_find)) ->
                              v_lhs := Some (compute_lhs
                                               (snd (List.hd args3))
                                               i nargsi)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 657efe175..cf0f51911 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -82,6 +82,7 @@ let lookup_map map =
     user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found")
 
 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);;
 
@@ -347,7 +348,7 @@ let find_ring_structure env sigma l =
         let ty = Retyping.get_type_of env sigma t in
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
-          if not (Reductionops.is_conv env sigma ty ty') then
+          if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then
             user_err ~hdr:"ring"
               (str"arguments of ring_simplify do not have all the same type")
         in
@@ -827,7 +828,7 @@ let find_field_structure env sigma l =
         let ty = Retyping.get_type_of env sigma t in
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
-          if not (Reductionops.is_conv env sigma ty ty') then
+          if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then
             user_err ~hdr:"field"
               (str"arguments of field_simplify do not have all the same type")
         in
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 86cc928c8..cc39b7260 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -481,7 +481,9 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 =
 (* p_origin can be passed to obtain a better error message     *)
 let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
   let k, f, a =
-    let f, a = Reductionops.whd_betaiota_stack ise p in
+    let f, a = Reductionops.whd_betaiota_stack ise (EConstr.of_constr p) in
+    let f = EConstr.Unsafe.to_constr f in
+    let a = List.map EConstr.Unsafe.to_constr a in
     match kind_of_term f with
     | Const (p,_) ->
       let np = proj_nparams p in