Tacmach API using EConstr.

33 files changed, 170 insertions, 144 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index c3ca8f906..3e7cf5d13 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -734,7 +734,7 @@ let refl_equal =
   call it before it is defined. *)
 let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
+    let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (EConstr.of_constr a)) gl in
        Tacticals.New.tclTHENLIST
          [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
           Proofview.Goal.nf_enter { enter = begin fun gl ->
@@ -789,7 +789,7 @@ let destauto t =
 
 let destauto_in id = 
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in
+  let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (EConstr.mkVar id)) gl in
 (*  Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
 (*  Pp.msgnl (Printer.pr_lconstr (ctype)); *)
   destauto ctype
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index dfcfbfbd3..37b9a9edb 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -2188,7 +2188,7 @@ let setoid_transitivity c =
     
 let setoid_symmetry_in id =
   Proofview.V82.tactic (fun gl ->
-  let ctype = pf_unsafe_type_of gl (mkVar id) in
+  let ctype = pf_unsafe_type_of gl (EConstr.mkVar id) in
   let binders,concl = decompose_prod_assum ctype in
   let (equiv, args) = decompose_app concl in
   let rec split_last_two = function
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 3ba5da149..1e49d8cad 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -179,6 +179,7 @@ module Btauto = struct
 
   let print_counterexample p env gl =
     let var = lapp witness [|p|] in
+    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 rec to_list l = match decomp_term (Tacmach.project gl) l with
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index bc53b113d..102efe55b 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -508,7 +508,7 @@ let rec add_term state t=
 	Not_found ->
 	  let b=next uf in
           let trm = constr_of_term t in
-	  let typ = pf_unsafe_type_of state.gls trm in
+	  let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in
 	  let typ = canonize_name typ in
 	  let new_node=
 	    match t with
@@ -832,7 +832,7 @@ let complete_one_class state i=
 	    let id = new_state_var etyp state in
 		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
 	let _c = pf_unsafe_type_of state.gls
-	  (constr_of_term (term state.uf pac.cnode)) in
+	  (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
 	let _args =
 	  List.map (fun i -> constr_of_term (term state.uf  i))
 	    pac.args in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 11da923e1..7c78f3a17 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -243,7 +243,8 @@ let app_global f args k =
 let new_app_global f args k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
-let new_refine c = Proofview.V82.tactic (refine c)
+let new_refine c = Proofview.V82.tactic (refine (EConstr.of_constr c))
+let refine c = refine (EConstr.of_constr c)
 
 let assert_before n c =
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -265,7 +266,7 @@ let refresh_universes ty k =
 
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
+  let type_of t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t) in
   try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> exact_check c
@@ -336,7 +337,7 @@ let refute_tac c t1 t2 p =
     let neweq= new_app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr tt1)) k
   end }
 
 let refine_exact_check c gl =
@@ -354,7 +355,7 @@ let convert_to_goal_tac c t1 t2 p =
     let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
 			   [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr tt2)) k
   end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -376,7 +377,7 @@ let discriminate_tac (cstr,u as cstru) p =
     let identity = Universes.constr_of_global (Lazy.force _I) in
     let trivial = Universes.constr_of_global (Lazy.force _True) in
     let evm = Tacmach.New.project gl in
-    let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in
+    let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t1))) in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 3bb6f1b5d..031a6253a 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -491,7 +491,7 @@ let thus_tac c ctyp submetas gls =
     Proofview.V82.of_tactic (exact_check proof) gls
   else
     let refiner = concl_refiner list proof gls in
-      Tacmach.refine refiner gls
+      Tacmach.refine (EConstr.of_constr refiner) gls
 
 (* general forward step *)
 
@@ -799,7 +799,7 @@ let rec take_tac wits gls =
   match wits with
       [] -> tclIDTAC gls
     | wit::rest ->
-	let typ = pf_unsafe_type_of gls wit in
+	let typ = pf_unsafe_type_of gls (EConstr.of_constr wit) in
 	  tclTHEN (thus_tac wit typ []) (take_tac rest)  gls
 
 
@@ -879,7 +879,7 @@ let start_tree env ind rp =
 let build_per_info etype casee gls =
   let concl=pf_concl gls in
   let env=pf_env gls in
-  let ctyp=pf_unsafe_type_of gls casee in
+  let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in
   let is_dep = dependent (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl) in
   let hd,args = decompose_app (special_whd gls ctyp) in
   let (ind,u) =
@@ -894,7 +894,7 @@ let build_per_info etype casee gls =
       | _ -> mind.mind_nparams,None in
   let params,real_args = List.chop nparams args in
   let abstract_obj c body =
-    let typ=pf_unsafe_type_of gls c in
+    let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
       lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in
   let pred= List.fold_right abstract_obj
     real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl))) in
@@ -1256,13 +1256,13 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let nparams = mind.mind_nparams in
 	let concl=pf_concl gls in
 	let env=pf_env gls in
-	let ctyp=pf_unsafe_type_of gls casee in
+	let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in
 	let hd,all_args = decompose_app (special_whd gls ctyp) in
 	let ind', u = destInd hd in
 	let _ = assert (eq_ind ind' ind) in (* just in case *)
 	let params,real_args = List.chop nparams all_args in
 	let abstract_obj c body =
-	  let typ=pf_unsafe_type_of gls c in
+	  let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
 	    lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in
 	let elim_pred = List.fold_right abstract_obj
 	  real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl))) in
@@ -1314,7 +1314,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 		       execute_cases fix_name per_info tacnext
 			 p_args objs nhrec tree] gls0 in
 	  tclTHENSV
-	    (refine case_term)
+	    (refine (EConstr.of_constr case_term))
 	    (Array.mapi branch_tac br) gls
     | Split_patt (_, _, _) , [] ->
 	anomaly ~label:"execute_cases " (Pp.str "Nothing to split")
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 44bdb585a..6c245063c 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -104,7 +104,7 @@ let mk_open_instance id idc gl m t=
   let evmap=Refiner.project gl in
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_unsafe_type_of gl idc in
+      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
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 1248b60a7..87e7192d7 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -200,7 +200,7 @@ let extend_with_ref_list l seq gl =
   let l = expand_constructor_hints l in
   let f gr (seq,gl) =
     let gl, c = pf_eapply Evd.fresh_global gl gr in
-    let typ=(pf_unsafe_type_of gl c) in
+    let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
       (add_formula Hyp gr typ seq gl,gl) in
     List.fold_right f l (seq,gl)
 
@@ -215,7 +215,7 @@ let extend_with_auto_hints l seq gl=
           let (c, _, _) = c in
 	  (try
 	     let gr = global_of_constr c in
-	     let typ=(pf_unsafe_type_of gl c) in
+	     let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
       | _-> () in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 83fc48623..b674f40e9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -202,6 +202,7 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) =
 	     (List.map mkVar context_hyps)
 	 in
 	 let to_refine = applist(mkVar h_id,List.rev context_hyps') in
+	 let to_refine = EConstr.of_constr to_refine in
 	 refine to_refine g
       )
     ]
@@ -329,7 +330,8 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	   let all_ids = pf_ids_of_hyps g in
 	   let new_ids,_  = list_chop ctxt_size all_ids in
 	   let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
-	   let evm, _ = pf_apply Typing.type_of g (EConstr.of_constr to_refine) in
+	   let to_refine = EConstr.of_constr to_refine in
+	   let evm, _ = pf_apply Typing.type_of g to_refine in
 	     tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g
 	)
     in
@@ -448,6 +450,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 			       List.rev_map mkVar (rec_pte_id::context_hyps_ids)
 			      )
 		     in
+		     let to_refine = EConstr.of_constr to_refine in
 (* 		     observe_tac "rec hyp " *)
 		       (tclTHENS
 		       (Proofview.V82.of_tactic (assert_before (Name rec_pte_id) t_x))
@@ -497,6 +500,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 			    List.rev (coq_I::List.map mkVar context_hyps)
 			   )
 		 in
+		 let to_refine = (EConstr.of_constr to_refine) in
 		 refine to_refine g
 	      )
 	    ]
@@ -594,7 +598,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps;
 	observe_tac "after_introduction" (fun g' ->
 	   (* We get infos on the equations introduced*)
-	   let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
+	   let new_term_value_eq = pf_unsafe_type_of g' (EConstr.mkVar heq_id) in
 	   (* compute the new value of the body *)
 	   let new_term_value =
 	     match kind_of_term new_term_value_eq with
@@ -605,13 +609,14 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 			   );
 		   anomaly (Pp.str "cannot compute new term value")
 	   in
+          let term = EConstr.of_constr term in
 	 let fun_body =
 	   mkLambda(Anonymous,
 		    pf_unsafe_type_of g' term,
-		    Termops.replace_term (project g') (EConstr.of_constr term) (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info)
+		    Termops.replace_term (project g') term (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info)
 		   )
 	 in
-	 let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
+	 let new_body = pf_nf_betaiota g' (EConstr.of_constr (mkApp(fun_body,[| new_term_value |]))) in
 	 let new_infos =
 	   {dyn_infos with
 	      info = new_body;
@@ -700,7 +705,7 @@ let build_proof
 		  let dyn_infos = {dyn_info' with info =
 		      mkCase(ci,ct,t,cb)} in
 		  let g_nb_prod = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in
-		  let type_of_term = pf_unsafe_type_of g t in
+		  let type_of_term = pf_unsafe_type_of g (EConstr.of_constr t) in
 		  let term_eq =
 		    make_refl_eq (Lazy.force refl_equal) type_of_term t
 		  in
@@ -741,7 +746,7 @@ let build_proof
 			   let id = pf_last_hyp g' |> get_id in
 			   let new_term =
 			     pf_nf_betaiota g'
-			       (mkApp(dyn_infos.info,[|mkVar id|]))
+			       (EConstr.of_constr (mkApp(dyn_infos.info,[|mkVar id|])))
 			   in
 			   let new_infos = {dyn_infos with info = new_term} in
 			   let do_prove new_hyps =
@@ -908,6 +913,7 @@ let prove_rec_hyp_for_struct fix_info =
 	   let rec_hyp_proof =
 	     mkApp(mkVar fix_info.name,array_get_start pte_args)
 	   in
+	   let rec_hyp_proof = EConstr.of_constr rec_hyp_proof in
 	   refine rec_hyp_proof g
 	))
 
@@ -921,7 +927,7 @@ let generalize_non_dep hyp g =
 (*   observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
   let hyps = [hyp] in
   let env = Global.env () in
-  let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in
+  let hyp_typ = pf_unsafe_type_of g (EConstr.mkVar hyp) in
   let to_revert,_ =
     let open Context.Named.Declaration in
     Environ.fold_named_context_reverse (fun (clear,keep) decl ->
@@ -1418,7 +1424,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
     let rewrite =
       tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
     in
-    let _,hrec_concl  = decompose_prod (pf_unsafe_type_of gls (mkVar hrec)) in
+    let _,hrec_concl  = decompose_prod (pf_unsafe_type_of gls (EConstr.mkVar hrec)) in
     let f_app = Array.last (snd (destApp hrec_concl)) in
     let f =  (fst (destApp f_app)) in
     let rec backtrack : tactic =
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 0743fc5d9..e3ba52246 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -75,11 +75,11 @@ let functional_induction with_clean c princl pat =
 		    user_err  (str "Cannot find induction principle for "
 				     ++Printer.pr_lconstr (mkConst c') )
 	      in
-	      (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g')
+	      (princ,NoBindings, Tacmach.pf_unsafe_type_of g' (EConstr.of_constr princ),g')
 	   | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
 	 end
       | Some ((princ,binding)) ->
-	 princ,binding,Tacmach.pf_unsafe_type_of g princ,g
+	 princ,binding,Tacmach.pf_unsafe_type_of g (EConstr.of_constr princ),g
     in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     let args_as_induction_constr =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e5286fb1f..635925562 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -305,7 +305,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let constructor_args g =
 	List.fold_right 
 	  (fun hid acc ->
-	     let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
+	     let type_of_hid = pf_unsafe_type_of g (EConstr.mkVar hid) in
 	     match kind_of_term type_of_hid with
 	       | Prod(_,_,t') ->
 		   begin
@@ -596,7 +596,7 @@ let rec reflexivity_with_destruct_cases g =
 	 match sc with
 	     None -> tclIDTAC g
 	   | Some id ->
-	       match kind_of_term  (pf_unsafe_type_of g (mkVar id)) with
+	       match kind_of_term  (pf_unsafe_type_of g (EConstr.mkVar id)) with
 		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
 		     if Equality.discriminable (pf_env g) (project g) t1 t2
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
@@ -661,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 graph_principle in
+    let princ_type = pf_unsafe_type_of g (EConstr.of_constr graph_principle) in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* Then we get the number of argument of the function
        and compute a fresh name for each of them
@@ -919,7 +919,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
    if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
 *)
 let revert_graph kn post_tac hid g =
-    let typ = pf_unsafe_type_of g (mkVar hid) in
+    let typ = pf_unsafe_type_of g (EConstr.mkVar hid) in
     match kind_of_term typ with
       | App(i,args) when isInd i ->
 	  let ((kn',num) as ind'),u = destInd i in
@@ -970,7 +970,7 @@ let revert_graph kn post_tac hid g =
 let functional_inversion kn hid fconst f_correct : tactic =
   fun g ->
     let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
-    let type_of_h = pf_unsafe_type_of g (mkVar hid) in
+    let type_of_h = pf_unsafe_type_of g (EConstr.mkVar hid) in
     match kind_of_term type_of_h with
       | App(eq,args) when eq_constr eq (make_eq ())  ->
 	  let pre_tac,f_args,res =
@@ -1022,7 +1022,7 @@ let invfun qhyp f g =
        Proofview.V82.of_tactic begin
 	Tactics.try_intros_until
 	  (fun hid -> Proofview.V82.tactic begin fun g ->
-	     let hyp_typ = pf_unsafe_type_of g (mkVar hid)  in
+	     let hyp_typ = pf_unsafe_type_of g (EConstr.mkVar hid)  in
 	     match kind_of_term hyp_typ with
 	       | App(eq,args) when eq_constr eq (make_eq ()) ->
 		   begin
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index bdbf0242d..b2c93a754 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -117,7 +117,7 @@ let pf_get_new_ids idl g =
 
 let compute_renamed_type gls c =
   rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
-    (pf_unsafe_type_of gls c)
+    (pf_unsafe_type_of gls (EConstr.of_constr c))
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
 let ano_id = Id.of_string "anonymous"
@@ -402,7 +402,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 	    Proofview.V82.of_tactic (clear to_intros);
 	    h_intros to_intros;
 	    (fun g' -> 
-	      let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
+	      let ty_teq = pf_unsafe_type_of g' (EConstr.mkVar heq) in
 	      let teq_lhs,teq_rhs =
 		let _,args = try destApp ty_teq with DestKO -> assert false in
 		args.(1),args.(2)
@@ -516,13 +516,13 @@ let rec prove_lt hyple g =
       in
       let h =
 	List.find (fun id ->
-          match decompose_app (pf_unsafe_type_of g (mkVar id)) with
+          match decompose_app (pf_unsafe_type_of g (EConstr.mkVar id)) with
             | _, t::_ -> eq_constr t varx
             | _ -> false
 	) hyple
       in
       let y =
-	List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (mkVar h))))) in
+	List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (EConstr.mkVar h))))) in
       observe_tclTHENLIST (str "prove_lt1")[
 	Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
 	observe_tac (str "prove_lt") (prove_lt hyple)
@@ -684,7 +684,7 @@ let mkDestructEq :
         if Id.List.mem id not_on_hyp || not (Termops.occur_term (project g) (EConstr.of_constr expr) (EConstr.of_constr (get_type decl)))
         then None else Some id) hyps in
   let to_revert_constr = List.rev_map mkVar to_revert in
-  let type_of_expr = pf_unsafe_type_of g expr in
+  let type_of_expr = pf_unsafe_type_of g (EConstr.of_constr expr) in
   let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
            to_revert_constr in
     pf_typel new_hyps (fun _ ->
@@ -839,7 +839,7 @@ let rec prove_le g =
 	let matching_fun = 
 	  pf_is_matching g
 	    (Pattern.PApp(Pattern.PRef (reference_of_constr (le ())),[|Pattern.PVar (destVar x);Pattern.PMeta None|])) in 
-	let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g)
+	let (h,t) = List.find (fun (_,t) -> matching_fun (EConstr.of_constr t)) (pf_hyps_types g)
 	in 
 	let y = 
 	  let _,args = decompose_app t in 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index d15449aef..b832250a5 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 t) (List.rev path) (pf_concl gl) in
+  let newc = context (fun i t -> pf_nf gl (EConstr.of_constr t)) (List.rev path) (pf_concl gl) in
   Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
 
 let focused_simpl path = focused_simpl path
@@ -644,7 +644,7 @@ let clever_rewrite_base_poly typ p result theorem gl =
 		       [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
        [abstracted])
   in
-  exact (applist(t,[mkNewMeta()])) gl
+  exact (EConstr.of_constr (applist(t,[mkNewMeta()]))) gl
 
 let clever_rewrite_base p result theorem gl =
   clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem gl
@@ -665,7 +665,7 @@ let clever_rewrite p vpath t gl =
   let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in
   let vargs = List.map (fun p -> occurrence p occ) vpath in
   let t' = applist(t, (vargs @ [abstracted])) in
-  exact (applist(t',[mkNewMeta()])) gl
+  exact (EConstr.of_constr (applist(t',[mkNewMeta()]))) gl
 
 let rec shuffle p (t1,t2) =
   match t1,t2 with
@@ -1384,7 +1384,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 typ) with Kapp(Z,[]) -> true | _ -> false end ->
+	when begin match destructurate_type (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
@@ -1659,7 +1659,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 typ) with
+	begin match destructurate_type (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
@@ -1720,7 +1720,7 @@ let destructure_hyps =
           | Kimp(t1,t2) ->
 	      (* t1 and t2 might be in Type rather than Prop.
 		 For t1, the decidability check will ensure being Prop. *)
-              if is_Prop (type_of t2)
+              if is_Prop (type_of (EConstr.of_constr t2))
               then
 		let d1 = decidability t1 in
 		Tacticals.New.tclTHENLIST [
@@ -1789,7 +1789,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 typ) with
+		    match destructurate_type (pf_nf (EConstr.of_constr typ)) with
 		    | Kapp(Nat,_) ->
                         Tacticals.New.tclTHENLIST [
 			  (simplest_elim
@@ -1806,7 +1806,7 @@ let destructure_hyps =
                         ]
 		    | _ -> loop lit
                   end else begin
-		    match destructurate_type (pf_nf typ) with
+		    match destructurate_type (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|]))
@@ -1849,7 +1849,7 @@ let destructure_goal =
 	      let dec = decidability t in
 	      Tacticals.New.tclTHEN
                 (Proofview.V82.tactic (Tacmach.refine
-		                         (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
+		                         (EConstr.of_constr (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))))
 	        intro
 	    with Undecidable -> Tactics.elim_type (build_coq_False ())
 	  in
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 4935fe4bb..f2d91bad3 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 typ) = Kapp("Z",[]) -> Req (t1,t2)
+      when destructurate (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/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 7f628f165..ace557a52 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1390,7 +1390,7 @@ let ssrpatterntac _ist (arg_ist,arg) gl =
   let concl0 = pf_concl gl in
   let (t, uc), concl_x =
     fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in
-  let gl, tty = pf_type_of gl t in
+  let gl, tty = pf_type_of gl (EConstr.of_constr t) in
   let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in
   Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ae53c12ae..24d4af89a 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1214,8 +1214,8 @@ let reduce_to_ind_gen allow_product env sigma t =
   in
   elimrec env t []
 
-let reduce_to_quantified_ind env sigma c = reduce_to_ind_gen true env sigma (EConstr.of_constr c)
-let reduce_to_atomic_ind env sigma c = reduce_to_ind_gen false env sigma (EConstr.of_constr c)
+let reduce_to_quantified_ind env sigma c = reduce_to_ind_gen true env sigma c
+let reduce_to_atomic_ind env sigma c = reduce_to_ind_gen false env sigma c
 
 let find_hnf_rectype env sigma t =
   let ind,t = reduce_to_atomic_ind env sigma t in
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index d32fcf491..3587ae281 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -75,12 +75,12 @@ val cbv_norm_flags : CClosure.RedFlags.reds ->  reduction_function
 (** [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)]
    with [I] an inductive definition;
    returns [I] and [t'] or fails with a user error *)
-val reduce_to_atomic_ind : env ->  evar_map -> types -> pinductive * types
+val reduce_to_atomic_ind : env ->  evar_map -> EConstr.types -> pinductive * types
 
 (** [reduce_to_quantified_ind env sigma t] puts [t] in the form
    [t'=(x1:A1)..(xn:An)(I args)] with [I] an inductive definition;
    returns [I] and [t'] or fails with a user error *)
-val reduce_to_quantified_ind : env ->  evar_map -> types -> pinductive * types
+val reduce_to_quantified_ind : env ->  evar_map -> EConstr.types -> pinductive * types
 
 (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
    [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *)
@@ -91,7 +91,7 @@ val reduce_to_atomic_ref :
   env ->  evar_map -> global_reference -> EConstr.types -> types
 
 val find_hnf_rectype : 
-  env ->  evar_map -> types -> pinductive * constr list
+  env ->  evar_map -> EConstr.types -> pinductive * constr list
 
 val contextually : bool -> occurrences * constr_pattern ->
   (patvar_map -> reduction_function) -> reduction_function
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index bc5f17bf5..5b9322bfe 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -95,7 +95,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv =
   let clenv = { clenv with evd = evd' } in
   tclTHEN
     (tclEVARS (Evd.clear_metas evd'))
-    (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
+    (refine_no_check (EConstr.of_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl
   end
 
 open Unification
diff --git a/proofs/logic.ml b/proofs/logic.ml
index c5d6e3e08..829c96296 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -490,6 +490,7 @@ and mk_arggoals sigma goal goalacc funty allargs =
 and mk_casegoals sigma goal goalacc p c =
   let env = Goal.V82.env sigma goal in
   let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in
+  let ct = EConstr.of_constr ct in
   let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in
   let indspec =
     try Tacred.find_hnf_rectype env sigma ct
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index c2ebb76d7..b732e5b9d 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -77,37 +77,36 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
   let sigma = Sigma.Unsafe.of_evar_map (project gls) in
-  let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma (EConstr.of_constr c) in
+  let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in
   (Sigma.to_evar_map sigma, c)
 
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_eapply f gls x = 
   on_sig gls (fun evm -> f (pf_env gls) evm x)
 let pf_reduce = pf_apply
-let pf_reduce' f gl c = pf_apply f gl (EConstr.of_constr c)
 let pf_e_reduce = pf_apply
 
-let pf_whd_all         = pf_reduce' whd_all
-let pf_hnf_constr                = pf_reduce' hnf_constr
-let pf_nf                        = pf_reduce' simpl
-let pf_nf_betaiota               = pf_reduce' (fun _ -> nf_betaiota)
-let pf_compute                   = pf_reduce' compute
-let pf_unfoldn ubinds            = pf_reduce' (unfoldn ubinds)
-let pf_unsafe_type_of            = pf_reduce' unsafe_type_of
-let pf_type_of                   = pf_reduce' type_of
+let pf_whd_all         = pf_reduce whd_all
+let pf_hnf_constr                = pf_reduce hnf_constr
+let pf_nf                        = pf_reduce simpl
+let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
+let pf_compute                   = pf_reduce compute
+let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
+let pf_unsafe_type_of            = pf_reduce unsafe_type_of
+let pf_type_of                   = pf_reduce type_of
 let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
-let pf_conv_x gl                = pf_apply test_conversion gl Reduction.CONV
+let pf_conv_x gl                = pf_reduce test_conversion gl Reduction.CONV
 let pf_conv_x_leq gl            = pf_reduce test_conversion gl Reduction.CUMUL
 let pf_const_value              = pf_reduce (fun env _ -> constant_value_in env)
 
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
-let pf_hnf_type_of gls          = EConstr.of_constr %> pf_get_type_of gls %> pf_whd_all gls
+let pf_hnf_type_of gls          = pf_get_type_of gls %> EConstr.of_constr %> pf_whd_all gls
 
-let pf_is_matching gl p c       = pf_apply Constr_matching.is_matching_conv gl p (EConstr.of_constr c)
-let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p (EConstr.of_constr c)
+let pf_is_matching gl p c       = pf_apply Constr_matching.is_matching_conv gl p c
+let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p c
 
 (********************************************)
 (* Definition of the most primitive tactics *)
@@ -116,12 +115,15 @@ let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p (EC
 let refiner = refiner
 
 let internal_cut_no_check replace id t gl =
+  let t = EConstr.Unsafe.to_constr t in
   refiner (Cut (true,replace,id,t)) gl
 
 let internal_cut_rev_no_check replace id t gl =
+  let t = EConstr.Unsafe.to_constr t in
   refiner (Cut (false,replace,id,t)) gl
 
 let refine_no_check c gl =
+  let c = EConstr.Unsafe.to_constr c in
   refiner (Refine c) gl
 
 (* Versions with consistency checks *)
@@ -159,9 +161,6 @@ module New = struct
   let pf_apply f gl =
     f (Proofview.Goal.env gl) (project gl)
 
-  let pf_reduce f gl c =
-    f (Proofview.Goal.env gl) (project gl) (EConstr.of_constr c)
-
   let of_old f gl =
     f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; }
 
@@ -175,10 +174,10 @@ module New = struct
   let pf_concl = Proofview.Goal.concl
 
   let pf_unsafe_type_of gl t =
-    pf_apply unsafe_type_of gl (EConstr.of_constr t)
+    pf_apply unsafe_type_of gl t
 
   let pf_type_of gl t =
-    pf_apply type_of gl (EConstr.of_constr t)
+    pf_apply type_of gl t
 
   let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2
 
@@ -221,18 +220,18 @@ module New = struct
     let sigma = project gl in
     nf_evar sigma concl
 
-  let pf_whd_all gl t = pf_reduce whd_all gl t
+  let pf_whd_all gl t = pf_apply whd_all gl t
 
   let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t
 
   let pf_reduce_to_quantified_ind gl t =
     pf_apply reduce_to_quantified_ind gl t
 
-  let pf_hnf_constr gl t = pf_reduce hnf_constr gl t
+  let pf_hnf_constr gl t = pf_apply hnf_constr gl t
   let pf_hnf_type_of gl t =
-    pf_whd_all gl (pf_get_type_of gl (EConstr.of_constr t))
+    pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t))
 
-  let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat (EConstr.of_constr t)
+  let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
 
   let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 16f6f88c1..07d02212c 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -40,9 +40,9 @@ val pf_nth_hyp_id         : goal sigma -> int -> Id.t
 val pf_last_hyp           : goal sigma -> Context.Named.Declaration.t
 val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
-val pf_unsafe_type_of            : goal sigma -> constr -> types
-val pf_type_of            : goal sigma -> constr -> evar_map * types
-val pf_hnf_type_of        : goal sigma -> constr -> types
+val pf_unsafe_type_of            : goal sigma -> EConstr.constr -> types
+val pf_type_of            : goal sigma -> EConstr.constr -> evar_map * types
+val pf_hnf_type_of        : goal sigma -> EConstr.constr -> types
 
 val pf_get_hyp            : goal sigma -> Id.t -> Context.Named.Declaration.t
 val pf_get_hyp_typ        : goal sigma -> Id.t -> types
@@ -50,7 +50,7 @@ val pf_get_hyp_typ        : goal sigma -> Id.t -> types
 val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
 val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list
 
-val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr
+val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * constr
 
 
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
@@ -63,35 +63,35 @@ val pf_e_reduce :
   (env -> evar_map -> constr -> evar_map * constr) ->
   goal sigma -> constr -> evar_map * constr
 
-val pf_whd_all       : goal sigma -> constr -> constr
-val pf_hnf_constr              : goal sigma -> constr -> constr
-val pf_nf                      : goal sigma -> constr -> constr
-val pf_nf_betaiota             : goal sigma -> constr -> constr
-val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types
-val pf_reduce_to_atomic_ind     : goal sigma -> types -> pinductive * types
-val pf_compute                 : goal sigma -> constr -> constr
+val pf_whd_all       : goal sigma -> EConstr.constr -> constr
+val pf_hnf_constr              : goal sigma -> EConstr.constr -> constr
+val pf_nf                      : goal sigma -> EConstr.constr -> constr
+val pf_nf_betaiota             : goal sigma -> EConstr.constr -> constr
+val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * types
+val pf_reduce_to_atomic_ind     : goal sigma -> EConstr.types -> pinductive * types
+val pf_compute                 : goal sigma -> EConstr.constr -> constr
 val pf_unfoldn    : (occurrences * evaluable_global_reference) list
-  -> goal sigma -> constr -> constr
+  -> goal sigma -> EConstr.constr -> constr
 
 val pf_const_value : goal sigma -> pconstant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
 val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
-val pf_matches     : goal sigma -> constr_pattern -> constr -> patvar_map
-val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
+val pf_matches     : goal sigma -> constr_pattern -> EConstr.constr -> patvar_map
+val pf_is_matching : goal sigma -> constr_pattern -> EConstr.constr -> bool
 
 
 (** {6 The most primitive tactics. } *)
 
 val refiner                   : rule -> tactic
-val internal_cut_no_check     : bool -> Id.t -> types -> tactic
-val refine_no_check           : constr -> tactic
+val internal_cut_no_check     : bool -> Id.t -> EConstr.types -> tactic
+val refine_no_check           : EConstr.constr -> tactic
 
 (** {6 The most primitive tactics with consistency and type checking } *)
 
-val internal_cut     : bool -> Id.t -> types -> tactic
-val internal_cut_rev : bool -> Id.t -> types -> tactic
-val refine           : constr -> tactic
+val internal_cut     : bool -> Id.t -> EConstr.types -> tactic
+val internal_cut_rev : bool -> Id.t -> EConstr.types -> tactic
+val refine           : EConstr.constr -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : goal sigma -> Pp.std_ppcmds
@@ -108,8 +108,8 @@ module New : sig
   val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
   val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
 
-  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
-  val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types
+  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> Term.types
+  val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * Term.types
   val pf_conv_x : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool
 
   val pf_get_new_id  : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier
@@ -121,15 +121,15 @@ module New : sig
   val pf_last_hyp           : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
 
   val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
-  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types
+  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * types
 
-  val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
-  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
+  val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types
+  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types
 
   val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr
   val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr
 
-  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
+  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map
 
   val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b0f355170..a2699ba8d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -226,7 +226,7 @@ let e_give_exact flags poly (c,clenv) gl =
         c, {gl with sigma = evd}
     else c, gl
   in
-  let t1 = pf_unsafe_type_of gl c in
+  let t1 = pf_unsafe_type_of gl (EConstr.of_constr c) in
   Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
 
 let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
@@ -1514,7 +1514,7 @@ let is_ground c gl =
 let autoapply c i gl =
   let flags = auto_unif_flags Evar.Set.empty
     (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
-  let cty = pf_unsafe_type_of gl c in
+  let cty = pf_unsafe_type_of gl (EConstr.of_constr c) in
   let ce = mk_clenv_from gl (c,cty) in
   let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl
     ((c,cty,Univ.ContextSet.empty),0,ce) } in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9580fdbfc..2058b95a6 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -113,7 +113,7 @@ let contradiction_term (c,lbind as cl) =
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
-    let typ = type_of c in
+    let typ = type_of (EConstr.of_constr c) in
     let _, ccl = splay_prod env sigma (EConstr.of_constr typ) in
     if is_empty_type sigma ccl then
       Tacticals.New.tclTHEN
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 0869ac0c7..2fad4fcf7 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -30,7 +30,7 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state
 
 let e_give_exact ?(flags=eauto_unif_flags) c =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let t1 = Tacmach.New.pf_unsafe_type_of gl c in
+  let t1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
   let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
   let sigma = Tacmach.New.project gl in
   if occur_existential sigma (EConstr.of_constr t1) || occur_existential sigma (EConstr.of_constr t2) then
diff --git a/tactics/elim.ml b/tactics/elim.ml
index b830ccefe..bcb1c05cc 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -80,7 +80,7 @@ let general_decompose recognizer c =
   Proofview.Goal.enter { enter = begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
   let sigma = project gl in
-  let typc = type_of c in
+  let typc = type_of (EConstr.of_constr c) in
   tclTHENS (cut typc)
     [ tclTHEN (intro_using tmphyp_name)
          (onLastHypId
@@ -133,7 +133,7 @@ let induction_trailer abs_i abs_j bargs =
     (onLastHypId
        (fun id ->
           Proofview.Goal.nf_enter { enter = begin fun gl ->
-	  let idty = pf_unsafe_type_of gl (mkVar id) in
+	  let idty = pf_unsafe_type_of gl (EConstr.mkVar id) in
 	  let fvty = global_vars (pf_env gl) (project gl) (EConstr.of_constr idty) in
 	  let possible_bring_hyps =
 	    (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 1554d43f0..d1b14a907 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -156,7 +156,7 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
   ]
 | a1 :: largs, a2 :: rargs ->
   Proofview.Goal.enter { enter = begin fun gl ->
-  let rectype = pf_unsafe_type_of gl a1 in
+  let rectype = pf_unsafe_type_of gl (EConstr.of_constr a1) in
   let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
   let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
   let subtacs =
@@ -226,7 +226,7 @@ let decideEquality rectype =
 
 let compare c1 c2 =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let rectype = pf_unsafe_type_of gl c1 in
+  let rectype = pf_unsafe_type_of gl (EConstr.of_constr c1) in
   let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
   (tclTHENS (cut decide)
             [(tclTHEN  intro
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 64b56b99b..ad80d2d1f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -181,8 +181,8 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
-  let sigma, ct = pf_type_of gl c in
-  let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in
+  let sigma, ct = pf_type_of gl (EConstr.of_constr c) in
+  let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma (EConstr.of_constr ct)) with UserError _ -> ct in
   let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
   [eqclause]
 
@@ -992,6 +992,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
   let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
+  let pf = EConstr.of_constr pf in
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.tclEFFECTS eff <*>
   tclTHENS (assert_after Anonymous absurd_term)
@@ -1012,8 +1013,8 @@ let onEquality with_evars tac (c,lbindc) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
-  let t = type_of c in
-  let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
+  let t = type_of (EConstr.of_constr c) in
+  let t' = try snd (reduce_to_quantified_ind (EConstr.of_constr t)) with UserError _ -> t in
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
   let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
@@ -1327,7 +1328,7 @@ let inject_if_homogenous_dependent_pair ty =
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
       pf_apply is_conv gl (EConstr.of_constr ar1.(2)) (EConstr.of_constr ar2.(2))) then raise Exit;
     Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
-    let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
+    let new_eq_args = [|pf_unsafe_type_of gl (EConstr.of_constr ar1.(3));ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
@@ -1339,7 +1340,7 @@ let inject_if_homogenous_dependent_pair ty =
         tclTHENS (cut (mkApp (ceq,new_eq_args)))
           [clear [destVar hyp];
            Proofview.V82.tactic (Tacmach.refine
-             (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
+             (EConstr.of_constr (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))))
           ])]
   with Exit ->
     Proofview.tclUNIT ()
@@ -1384,7 +1385,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       (Proofview.tclIGNORE (Proofview.Monad.List.map
          (fun (pf,ty) -> tclTHENS (cut ty)
            [inject_if_homogenous_dependent_pair ty;
-            Proofview.V82.tactic (Tacmach.refine pf)])
+            Proofview.V82.tactic (Tacmach.refine (EConstr.of_constr pf))])
          (if l2r then List.rev injectors else injectors)))
       (tac (List.length injectors)))
 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 87e252a38..5d78fd585 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -437,7 +437,7 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *)
 
 let extract_eq_args gl = function
   | MonomorphicLeibnizEq (e1,e2) ->
-      let t = pf_unsafe_type_of gl e1 in (t,e1,e2)
+      let t = pf_unsafe_type_of gl (EConstr.of_constr e1) in (t,e1,e2)
   | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
   | HeterogenousEq (t1,e1,t2,e2) ->
       if pf_conv_x gl (EConstr.of_constr t1) (EConstr.of_constr t2) then (t1,e1,e2)
@@ -463,6 +463,7 @@ let match_eq_nf gls eqn (ref, hetero) =
   let n = if hetero then 4 else 3 in
   let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in
   let pat = mkPattern (mkGAppRef ref args) in
+  let eqn = EConstr.of_constr eqn in
   match Id.Map.bindings (pf_matches gls pat eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
diff --git a/tactics/inv.ml b/tactics/inv.ml
index eebc67222..2f5186f81 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -438,7 +438,7 @@ let raw_inversion inv_kind id status names =
     let concl = Proofview.Goal.concl gl in
     let c = mkVar id in
     let (ind, t) =
-      try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
+      try pf_apply Tacred.reduce_to_atomic_ind gl (EConstr.of_constr (pf_unsafe_type_of gl (EConstr.of_constr c)))
       with UserError _ ->
         let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
         CErrors.user_err  msg
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 2754db010..02909243d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -628,7 +628,7 @@ module New = struct
     (Proofview.Goal.nf_enter { enter = begin fun gl ->
     let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
     (* applying elimination_scheme just a little modified *)
-    let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in
+    let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elim))) gl in
     let indmv =
       match kind_of_term (last_arg elimclause.evd (EConstr.of_constr elimclause.templval.Evd.rebus)) with
       | Meta mv -> mv
@@ -678,7 +678,7 @@ module New = struct
 
   let elimination_then tac c =
     Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
+    let (ind,t) = pf_reduce_to_quantified_ind gl (EConstr.of_constr (pf_unsafe_type_of gl (EConstr.of_constr c))) in
     let isrec,mkelim =
       match (Global.lookup_mind (fst (fst ind))).mind_record with
       | None -> true,gl_make_elim
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 639a12b34..b9a219a2c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -457,6 +457,7 @@ let assert_before_then_gen b naming t tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
     let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
+    let t = EConstr.of_constr t in
     Tacticals.New.tclTHENLAST
       (Proofview.V82.tactic
          (fun gl ->
@@ -476,6 +477,7 @@ let assert_after_then_gen b naming t tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
     let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
+    let t = EConstr.of_constr t in
     Tacticals.New.tclTHENFIRST
       (Proofview.V82.tactic
          (fun gl ->
@@ -1303,6 +1305,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
   if not with_evars && occur_meta clenv.evd (EConstr.of_constr new_hyp_typ) then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
+  let new_hyp_prf = EConstr.of_constr new_hyp_prf in
   let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in
   let naming = NamingMustBe (dloc,targetid) in
   let with_clear = do_replace (Some id) naming in
@@ -1434,7 +1437,7 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let ct = Retyping.get_type_of env sigma (EConstr.of_constr c) in
-  let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in
+  let t = try snd (reduce_to_quantified_ind env sigma (EConstr.of_constr ct)) with UserError _ -> ct in
   let elimtac = elimination_clause_scheme with_evars in
   let indclause  = make_clenv_binding env sigma (c, t) lbindc in
   let sigma = meta_merge sigma (clear_metas indclause.evd) in
@@ -1452,6 +1455,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
   let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) (EConstr.of_constr c) in
+  let t = EConstr.of_constr t in
   let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in
   let sort = Tacticals.New.elimination_sort_of_goal gl in
   let Sigma (elim, sigma, p) =
@@ -1491,7 +1495,8 @@ let find_ind_eliminator ind s gl =
     evd, c
 
 let find_eliminator c gl =
-  let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
+  let c = EConstr.of_constr c in
+  let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl c)) in
   if is_nonrec ind then raise IsNonrec;
   let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
     evd, {elimindex = None; elimbody = (c,NoBindings);
@@ -1637,6 +1642,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
   let sigma = Tacmach.New.project gl in
   try
     let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
+    let t = EConstr.of_constr t in
     let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
     let sign,ccl = decompose_prod_assum t in
     match match_with_tuple sigma ccl with
@@ -1661,6 +1667,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
 	    match make_projection env sigma params cstr sign elim i n c u with
 	    | None -> Tacticals.New.tclFAIL 0 (mt())
 	    | Some (p,pt) ->
+              let p = EConstr.of_constr p in
 	      Tacticals.New.tclTHENS
 		(assert_before_gen false (NamingAvoid avoid) pt)
 		[Proofview.V82.tactic (refine p);
@@ -1920,7 +1927,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
 let cut_and_apply c =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
-    match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with
+    match kind_of_term (Tacmach.New.pf_hnf_constr gl (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c)))) with
       | Prod (_,c1,c2) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr c2) ->
         let concl = Proofview.Goal.concl gl in
         let env = Tacmach.New.pf_env gl in
@@ -2201,6 +2208,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
     let reduce_to_quantified_ind =
       Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
     in
+    let cl = EConstr.of_constr cl in
     let (mind,redcl) = reduce_to_quantified_ind cl in
     let nconstr =
       Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
@@ -2240,6 +2248,7 @@ let any_constructor with_evars tacopt =
     let reduce_to_quantified_ind =
       Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
     in
+    let cl = EConstr.of_constr cl in
     let mind = fst (reduce_to_quantified_ind cl) in
     let nconstr =
       Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
@@ -2298,7 +2307,8 @@ let my_find_eq_data_decompose gl t =
 let intro_decomp_eq loc l thin tac id =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let c = mkVar id in
-  let t = Tacmach.New.pf_unsafe_type_of gl c in
+  let t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
+  let t = EConstr.of_constr t in
   let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
   match my_find_eq_data_decompose gl t with
   | Some (eq,u,eq_args) ->
@@ -2312,7 +2322,8 @@ let intro_decomp_eq loc l thin tac id =
 let intro_or_and_pattern loc with_evars bracketed ll thin tac id =
   Proofview.Goal.enter { enter = begin fun gl ->
   let c = mkVar id in
-  let t = Tacmach.New.pf_unsafe_type_of gl c in
+  let t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
+  let t = EConstr.of_constr t in
   let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
   let branchsigns = compute_constructor_signatures false ind in
   let nv_with_let = Array.map List.length branchsigns in
@@ -2337,7 +2348,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
     let sigma = Tacmach.New.project gl in
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let whd_all = Tacmach.New.pf_apply whd_all gl in
-    let t = whd_all (EConstr.of_constr (type_of (mkVar id))) in
+    let t = whd_all (EConstr.of_constr (type_of (EConstr.mkVar id))) in
     let eqtac, thin = match match_with_equality_type sigma t with
     | Some (hdcncl,[_;lhs;rhs]) ->
         if l2r && isVar lhs && not (occur_var env sigma (destVar lhs) (EConstr.of_constr rhs)) then
@@ -2747,7 +2758,7 @@ let forward b usetac ipat c =
   match usetac with
   | None ->
       Proofview.Goal.enter { enter = begin fun gl ->
-      let t = Tacmach.New.pf_unsafe_type_of gl c in
+      let t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
       let hd = head_ident c in
       Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c)
       end }
@@ -3233,7 +3244,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
             | Var id -> id
             | _ ->
             let type_of = Tacmach.New.pf_unsafe_type_of gl in
-            id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
+            id_of_name_using_hdchar (Global.env()) (type_of (EConstr.of_constr c)) Anonymous in
             let x = fresh_id_in_env avoid id env in
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) c None allHypsAndConcl)
@@ -3645,7 +3656,7 @@ let abstract_args gl generalize_vars dep id defined f args =
       let decl = List.hd rel in
       RelDecl.get_name decl, RelDecl.get_type decl, c
     in
-    let argty = Tacmach.pf_unsafe_type_of gl arg in
+    let argty = Tacmach.pf_unsafe_type_of gl (EConstr.of_constr arg) in
     let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma (EConstr.of_constr ty) in
     let () = sigma := sigma' in
     let lenctx = List.length ctx in
@@ -3686,7 +3697,7 @@ let abstract_args gl generalize_vars dep id defined f args =
 	      true, mkApp (f', before), after
   in
     if dogen then
-      let tyf' = Tacmach.pf_unsafe_type_of gl f' in
+      let tyf' = Tacmach.pf_unsafe_type_of gl (EConstr.of_constr f') in
       let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
 	Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
       in
@@ -3794,6 +3805,7 @@ let specialize_eqs id gl =
   let ty' = Tacred.whd_simpl env !evars (EConstr.of_constr ty')
   and acc' = Tacred.whd_simpl env !evars (EConstr.of_constr acc') in
   let ty' = Evarutil.nf_evar !evars ty' in
+  let ty' = EConstr.of_constr ty' in
     if worked then
       tclTHENFIRST (Tacmach.internal_cut true id ty')
 	(Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl
@@ -4014,6 +4026,7 @@ let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info =
 
 let guess_elim isrec dep s hyp0 gl =
   let tmptyp0 =	Tacmach.New.pf_get_hyp_typ hyp0 gl in
+  let tmptyp0 = EConstr.of_constr tmptyp0 in
   let mind,_ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in
   let evd, elimc =
     if isrec && not (is_nonrec (fst mind)) then find_ind_eliminator (fst mind) s gl
@@ -4028,12 +4041,13 @@ let guess_elim isrec dep s hyp0 gl =
         let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma mind s in
         (Sigma.to_evar_map sigma, ind)
   in
-  let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
+  let elimt = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elimc) in
     evd, ((elimc, NoBindings), elimt), mkIndU mind
 
 let given_elim hyp0 (elimc,lbind as e) gl =
   let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
   let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in
+  let elimc = EConstr.of_constr elimc in
   Tacmach.New.project gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess
 
 type scheme_signature =
@@ -4069,7 +4083,7 @@ let get_elim_signature elim hyp0 gl =
   compute_elim_signature (given_elim hyp0 elim gl) hyp0
 
 let is_functional_induction elimc gl =
-  let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in
+  let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr (fst elimc))) in
   (* The test is not safe: with non-functional induction on non-standard
      induction scheme, this may fail *)
   Option.is_empty scheme.indarg
@@ -4466,7 +4480,7 @@ let induction_gen_l isrec with_evars elim names lc =
                 let type_of = Tacmach.New.pf_unsafe_type_of gl in
                 let sigma = Tacmach.New.project gl in
                 let x =
-		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
+		  id_of_name_using_hdchar (Global.env()) (type_of (EConstr.of_constr c)) Anonymous in
 
                 let id = new_fresh_id [] x gl in
 		let newl' = List.map (fun r -> replace_term sigma (EConstr.of_constr c) (EConstr.mkVar id) (EConstr.of_constr r)) l' in
@@ -4606,6 +4620,7 @@ let elim_scheme_type elim t =
 
 let elim_type t =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  let t = EConstr.of_constr t in
   let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in
   let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in
   Sigma.Unsafe.of_pair (elim_scheme_type elimc t, evd)
@@ -4613,6 +4628,7 @@ let elim_type t =
 
 let case_type t =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  let t = EConstr.of_constr t in
   let sigma = Proofview.Goal.sigma gl in
   let env = Tacmach.New.pf_env gl in
   let (ind,t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in
@@ -4717,7 +4733,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 let symmetry_in id =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
+  let ctype = Tacmach.New.pf_unsafe_type_of gl (EConstr.mkVar id) in
   let sign,t = decompose_prod_assum ctype in
   Proofview.tclORELSE
     begin
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 02c43aec5..6561627f6 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -363,7 +363,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
       )
   in
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in
+    let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl (EConstr.of_constr p)) gl in
     let u,v = destruct_ind type_of_pq
     in let lb_type_of_p =
         try
@@ -425,7 +425,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
     match (l1,l2) with
     | (t1::q1,t2::q2) ->
         Proofview.Goal.enter { enter = begin fun gl ->
-        let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
+        let tt1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t1) in
         if eq_constr t1 t2 then aux q1 q2
         else (
           let u,v = try  destruct_ind tt1
diff --git a/toplevel/command.ml b/toplevel/command.ml
index dbf256ba8..80f3b26e4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1164,7 +1164,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
       List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
-      Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
+      Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC)
         fixdefs) in
     let init_tac =
       Option.map (List.map Proofview.V82.tactic) init_tac
@@ -1201,7 +1201,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
       List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
-      Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
+      Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC)
         fixdefs) in
     let init_tac =
       Option.map (List.map Proofview.V82.tactic) init_tac