Removing various compatibility layers of tactics.

20 files changed, 106 insertions, 88 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 0a980c03b..aedcb7575 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -452,8 +452,9 @@ and applist_projection c l =
       applistc (mkProj (p, hd)) tl)
   | _ -> applistc c l
 
-let rec canonize_name c =
-  let func =  canonize_name in
+let rec canonize_name sigma c =
+  let c = EConstr.Unsafe.to_constr c in
+  let func c = canonize_name sigma (EConstr.of_constr c) in
     match kind_of_term c with
       | Const (kn,u) ->
 	  let canon_const = constant_of_kn (canonical_con kn) in 
@@ -509,7 +510,7 @@ let rec add_term state t=
 	  let b=next uf in
           let trm = constr_of_term t in
 	  let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in
-	  let typ = canonize_name typ in
+	  let typ = canonize_name (project state.gls) typ in
 	  let new_node=
 	    match t with
 		Symb _ | Product (_,_) ->
@@ -833,6 +834,7 @@ let complete_one_class state i=
 		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
 	let _c = pf_unsafe_type_of state.gls
 	  (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
+        let _c = EConstr.Unsafe.to_constr _c 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 62892973d..2ab4dced4 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -219,7 +219,7 @@ let make_prb gls depth additionnal_terms =
 	     | `Nrule patts -> add_quant state id false patts
 	 end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it));
     begin
-      match atom_of_constr env sigma (EConstr.of_constr (pf_concl gls)) with
+      match atom_of_constr env sigma (pf_concl gls) with
 	  `Eq (t,a,b) -> add_disequality state Goal a b
 	|	`Other g ->
 		  List.iter
@@ -271,7 +271,7 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c)
 
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let type_of t = EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t) in
+  let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
   try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> exact_check (EConstr.of_constr c)
@@ -343,7 +343,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 (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl tt1)) k
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
   end }
 
 let refine_exact_check c gl =
@@ -361,7 +361,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 (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl tt2)) k
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
   end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -385,7 +385,7 @@ let discriminate_tac (cstr,u as cstru) p =
     let trivial = Universes.constr_of_global (Lazy.force _True) in
     let trivial = EConstr.of_constr trivial 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 (Tacmach.New.pf_unsafe_type_of gl 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 7123ebcaf..6a0ec3968 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -74,7 +74,7 @@ let tcl_change_info_gen info_gen =
      let concl = pf_concl gls in
      let hyps = Goal.V82.hyps (project gls) it in
      let extra = Goal.V82.extra (project gls) it in
-     let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps (EConstr.of_constr concl) (info_gen extra) in
+     let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in
      let sigma = Goal.V82.partial_solution sigma it ev in
      { it = [gl] ; sigma= sigma; } )
 
@@ -88,7 +88,7 @@ let tcl_erase_info gls =
 
 let special_whd gl=
   let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
-    (fun t -> CClosure.whd_val infos (CClosure.inject t))
+    (fun t -> CClosure.whd_val infos (CClosure.inject (EConstr.Unsafe.to_constr t)))
 
 let special_nf gl=
   let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
@@ -342,7 +342,7 @@ let rec replace_in_list m l = function
   | c::q -> if Int.equal m (fst c) then l@q else c::replace_in_list m l q
 
 let enstack_subsubgoals env se stack gls=
-  let hd,params = decompose_app (special_whd gls se.se_type) in
+  let hd,params = decompose_app (special_whd gls (EConstr.of_constr se.se_type)) in
     match kind_of_term hd with
 	Ind (ind,u as indu) when is_good_inductive env ind -> (* MS: FIXME *)
 	  let mib,oib=
@@ -397,6 +397,7 @@ let rec nf_list evd =
 let find_subsubgoal c ctyp skip submetas gls =
   let env= pf_env gls in
   let concl = pf_concl gls in
+  let concl = EConstr.Unsafe.to_constr concl in
   let evd = mk_evd ((0,concl)::submetas) gls in
   let stack = Stack.create () in
   let max_meta =
@@ -412,7 +413,7 @@ let find_subsubgoal c ctyp skip submetas gls =
       try
 	let unifier =
 	  Unification.w_unify env se.se_evd Reduction.CUMUL
-	    ~flags:(Unification.elim_flags ()) (EConstr.of_constr ctyp) (EConstr.of_constr se.se_type) in
+	    ~flags:(Unification.elim_flags ()) ctyp (EConstr.of_constr se.se_type) in
 	  if n <= 0 then
 	      {se with
 		 se_evd=meta_assign se.se_meta
@@ -433,7 +434,8 @@ let concl_refiner metas body gls =
   let concl = pf_concl gls in
   let evd = sig_sig gls in
   let env = pf_env gls in
-  let sort = family_of_sort (Typing.e_sort_of env (ref evd) (EConstr.of_constr concl)) in
+  let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in
+  let concl = EConstr.Unsafe.to_constr concl in
   let rec aux env avoid subst = function
       [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
     | (n,typ)::rest ->
@@ -504,7 +506,7 @@ let mk_stat_or_thesis info gls = function
     This c -> c
   | Thesis (For _ ) ->
       error "\"thesis for ...\" is not applicable here."
-  | Thesis Plain -> pf_concl gls
+  | Thesis Plain -> EConstr.Unsafe.to_constr (pf_concl gls)
 
 let just_tac _then cut info gls0 =
   let last_item =
@@ -536,7 +538,7 @@ let instr_cut mkstat _thus _then cut gls0 =
   let c_stat = mkstat info gls0 stat.st_it in
   let thus_tac gls=
     if _thus then
-      thus_tac (mkVar c_id) c_stat [] gls
+      thus_tac (mkVar c_id) (EConstr.of_constr c_stat) [] gls
     else tclIDTAC gls in
     tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat))
       [tclTHEN tcl_erase_info (just_tac _then cut info);
@@ -582,7 +584,7 @@ let instr_rew _thus rew_side cut gls0 =
     | Name id -> id,true in
   let thus_tac new_eq gls=
     if _thus then
-      thus_tac (mkVar c_id) new_eq [] gls
+      thus_tac (mkVar c_id) (EConstr.of_constr new_eq) [] gls
     else tclIDTAC gls in
     match rew_side with
 	Lhs ->
@@ -610,7 +612,7 @@ let instr_claim _thus st gls0 =
     | Name id -> id,true in
   let thus_tac gls=
     if _thus then
-      thus_tac (mkVar id) st.st_it [] gls
+      thus_tac (mkVar id) (EConstr.of_constr st.st_it) [] gls
     else tclIDTAC gls in
   let ninfo1 = {pm_stack=
       (if _thus then Focus_claim else Claim)::info.pm_stack} in
@@ -704,7 +706,7 @@ let instr_suffices _then cut gls0 =
   let c_ctx,c_head = build_applist c_stat metas in
   let c_term = applist (mkVar c_id,List.map mkMeta metas) in
   let thus_tac gls=
-    thus_tac c_term c_head c_ctx gls in
+    thus_tac c_term (EConstr.of_constr c_head) c_ctx gls in
    tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat))
      [tclTHENLIST
 	 [ assume_tac ctx;
@@ -891,8 +893,9 @@ 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 (EConstr.of_constr casee) in
-  let is_dep = dependent (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl) in
+  let is_dep = dependent (project gls) (EConstr.of_constr casee) concl in
   let hd,args = decompose_app (special_whd gls ctyp) in
+  let ctyp = EConstr.Unsafe.to_constr ctyp in
   let (ind,u) =
     try
       destInd hd
@@ -906,9 +909,10 @@ let build_per_info etype casee gls =
   let params,real_args = List.chop nparams args in
   let abstract_obj c body =
     let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
+    let typ = EConstr.Unsafe.to_constr typ 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
+    real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) concl)) in
     is_dep,
   {per_casee=casee;
    per_ctype=ctyp;
@@ -963,6 +967,7 @@ let register_nodep_subcase id= function
 let suppose_tac hyps gls0 =
   let info = get_its_info gls0 in
   let thesis = pf_concl gls0 in
+  let thesis = EConstr.Unsafe.to_constr thesis in
   let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
   let clause = build_product (project gls0) hyps thesis in
   let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
@@ -1132,7 +1137,7 @@ let rec build_product_dep pat_info per_info args body gls =
 		  with Not_found ->
 		    snd (st_assoc (Name id) pat_info.pat_aliases) in
 		  thesis_for obj typ per_info (pf_env gls)
-	    | Plain -> pf_concl gls in
+	    | Plain -> EConstr.Unsafe.to_constr (pf_concl gls) in
 	  mkProd (st.st_label,ptyp,lbody)
     | [] -> body
 
@@ -1225,6 +1230,7 @@ let pop_stacks stacks =
 let hrec_for fix_id per_info gls obj_id =
   let obj=mkVar obj_id in
   let typ=pf_get_hyp_typ gls obj_id in
+  let typ = EConstr.Unsafe.to_constr typ in
   let rc,hd1=decompose_prod typ in
   let cind,all_args=decompose_app typ in
   let ind,u = destInd cind in assert (eq_ind ind per_info.per_ind);
@@ -1269,14 +1275,16 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let env=pf_env gls 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 ctyp = EConstr.Unsafe.to_constr 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 (EConstr.of_constr c) in
+	  let typ = EConstr.Unsafe.to_constr typ 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
+	  real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) concl)) in
 	let case_info = Inductiveops.make_case_info env ind RegularStyle in
 	let gen_arities = Inductive.arities_of_constructors (ind,u) spec in
 	let f_ids typ =
@@ -1341,13 +1349,13 @@ let understand_my_constr env sigma c concl =
     | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None)
     | rc ->  map_glob_constr frob rc
   in
-  Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType (EConstr.of_constr concl)) (frob rawc)
+  Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc)
 
 let my_refine c gls =
   let oc = { run = begin fun sigma ->
     let sigma = Sigma.to_evar_map sigma in
     let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
-    Sigma.Unsafe.of_pair (EConstr.of_constr c, sigma)
+    Sigma.Unsafe.of_pair (c, sigma)
   end } in
   Proofview.V82.of_tactic (Tactics.New.refine oc) gls
 
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e39d17b52..f23f4ce7d 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -37,6 +37,7 @@ let start_deriving f suchthat lemma =
         let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
         let evdref = ref sigma in
         let suchthat = Constrintern.interp_type_evars env' evdref suchthat in
+        let suchthat = EConstr.Unsafe.to_constr suchthat in
         TCons ( env' , !evdref , suchthat , (fun sigma _ ->
         TNil sigma))))))
     in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 24d4346d9..2881b5333 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 (EConstr.Unsafe.to_constr (whd_all env evmap (EConstr.of_constr typ))) in
+      let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index bed7a727f..38dae0b20 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -38,14 +38,14 @@ let wrap n b continue seq gls=
 	  []->anomaly (Pp.str "Not the expected number of hyps")
 	| nd::q->
             let id = NamedDecl.get_id nd in
-	    if occur_var env (project gls) id (EConstr.of_constr (pf_concl gls)) ||
+	    if occur_var env (project gls) id (pf_concl gls) ||
 	      List.exists (occur_var_in_decl env (project gls)  id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
 	      add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in
   let seq1=aux n nc [] in
   let seq2=if b then
-    add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
+    add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in
     continue seq2 gls
 
 let basename_of_global=function
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 91cd102a2..fb0c22c2b 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -201,6 +201,7 @@ let extend_with_ref_list l seq gl =
   let f gr (seq,gl) =
     let gl, c = pf_eapply Evd.fresh_global gl gr in
     let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
+    let typ = EConstr.Unsafe.to_constr typ in
       (add_formula Hyp gr typ seq gl,gl) in
     List.fold_right f l (seq,gl)
 
@@ -216,6 +217,7 @@ let extend_with_auto_hints l seq gl=
 	  (try
 	     let (gr, _) = Termops.global_of_constr (project gl) c in
 	     let typ=(pf_unsafe_type_of gl c) in
+	     let typ = EConstr.Unsafe.to_constr typ 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 656924e38..f4fa61a22 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -394,7 +394,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
   *)
   let test_var g =
     let sigma = project g in
-    let _,args = destApp sigma (EConstr.of_constr (pf_concl g)) in
+    let _,args = destApp sigma (pf_concl g) in
     not ((isConstruct sigma args.(arg_num)) || isAppConstruct sigma args.(arg_num))
   in
   let rec do_rewrite eq_ids g  =
@@ -551,7 +551,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
       tclIDTAC
   in
   try
-    scan_type [] (EConstr.of_constr (Typing.unsafe_type_of env sigma (mkVar hyp_id))), [hyp_id]
+    scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id]
   with TOREMOVE ->
     thin [hyp_id],[]
 
@@ -602,7 +602,6 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	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 = EConstr.of_constr new_term_value_eq in
 	   (* compute the new value of the body *)
 	   let new_term_value =
 	     match EConstr.kind (project g') new_term_value_eq with
@@ -615,7 +614,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	   in
 	 let fun_body =
 	   mkLambda(Anonymous,
-		    EConstr.of_constr (pf_unsafe_type_of g' term),
+		    pf_unsafe_type_of g' term,
 		    Termops.replace_term (project g') term (mkRel 1) dyn_infos.info
 		   )
 	 in
@@ -708,9 +707,8 @@ let build_proof
 		  let t = dyn_info'.info in
 		  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 g_nb_prod = nb_prod (project g) (pf_concl g) in
 		  let type_of_term = pf_unsafe_type_of g t in
-		  let type_of_term = EConstr.of_constr type_of_term in
 		  let term_eq =
 		    make_refl_eq (Lazy.force refl_equal) type_of_term t
 		  in
@@ -722,7 +720,7 @@ let build_proof
 		      (fun g -> observe_tac "toto" (
 			 tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
 				     (fun g' ->
-					let g'_nb_prod = nb_prod (project g') (EConstr.of_constr (pf_concl g')) in
+					let g'_nb_prod = nb_prod (project g') (pf_concl g') in
 					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
 			 		observe_tac "treat_new_case"
 					  (treat_new_case
@@ -742,7 +740,7 @@ let build_proof
 	      build_proof do_finalize_t {dyn_infos with info = t} g
 	  | Lambda(n,t,b) ->
 	      begin
-		match EConstr.kind sigma (EConstr.of_constr ( pf_concl g)) with
+		match EConstr.kind sigma (pf_concl g) with
 		  | Prod _ ->
 		      tclTHEN
 			(Proofview.V82.of_tactic intro)
@@ -914,7 +912,7 @@ let prove_rec_hyp_for_struct fix_info =
       (fun  eq_hyps -> tclTHEN
 	(rewrite_until_var (fix_info.idx) eq_hyps)
 	(fun g ->
-	   let _,pte_args = destApp (project g) (EConstr.of_constr (pf_concl g)) in
+	   let _,pte_args = destApp (project g) (pf_concl g) in
 	   let rec_hyp_proof =
 	     mkApp(mkVar fix_info.name,array_get_start pte_args)
 	   in
@@ -938,7 +936,7 @@ let generalize_non_dep hyp g =
       let hyp = get_id decl in
       if Id.List.mem hyp hyps
         || List.exists (Termops.occur_var_in_decl env (project g) hyp) keep
-	|| Termops.occur_var env (project g) hyp (EConstr.of_constr hyp_typ)
+	|| Termops.occur_var env (project g) hyp hyp_typ
 	|| Termops.is_section_variable hyp (* should be dangerous *)
       then (clear,decl::keep)
       else (hyp::clear,keep))
@@ -1054,7 +1052,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
       let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in 
       res
   in
-  let nb_intro_to_do = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in
+  let nb_intro_to_do = nb_prod (project g) (pf_concl g) in
     tclTHEN
       (tclDO nb_intro_to_do (Proofview.V82.of_tactic intro))
       (
@@ -1070,7 +1068,6 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnames all_funs _nparams : tactic =
   fun g ->
   let princ_type = pf_concl g in
-  let princ_type = EConstr.of_constr princ_type in
   (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *)
   (* Pp.msgnl (str "all_funs "); *)
   (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *)
@@ -1258,7 +1255,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
     in
     let intros_after_fixes : tactic =
       fun gl ->
-	let ctxt,pte_app =  (decompose_prod_assum (project gl) (EConstr.of_constr (pf_concl gl))) in
+	let ctxt,pte_app =  (decompose_prod_assum (project gl) (pf_concl gl)) in
 	let pte,pte_args = (decompose_app (project gl) pte_app) in
 	try
 	  let pte =
@@ -1431,12 +1428,12 @@ 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 (project gls) (EConstr.of_constr (pf_unsafe_type_of gls (mkVar hrec))) in
+    let _,hrec_concl  = decompose_prod (project gls) (pf_unsafe_type_of gls (mkVar hrec)) in
     let f_app = Array.last (snd (destApp (project gls) hrec_concl)) in
     let f =  (fst (destApp (project gls) f_app)) in
     let rec backtrack : tactic =
       fun g ->
-	let f_app = Array.last (snd (destApp (project g) (EConstr.of_constr (pf_concl g)))) in
+	let f_app = Array.last (snd (destApp (project g) (pf_concl g))) in
 	match EConstr.kind (project g) f_app with
 	  | App(f',_) when eq_constr (project g) f' f -> tclIDTAC g
 	  | _ -> tclTHEN rewrite backtrack g
@@ -1525,7 +1522,6 @@ let prove_principle_for_gen
     (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
     rec_arg_num rec_arg_type relation gl =
   let princ_type = pf_concl gl in
-  let princ_type = EConstr.of_constr princ_type in
   let princ_info = compute_elim_sig (project gl) princ_type in
   let fresh_id =
     let avoid = ref (pf_ids_of_hyps gl) in
@@ -1664,7 +1660,7 @@ let prove_principle_for_gen
       Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
       (* observe_tac "finish" *) (fun gl' ->
 	 let body =
-	   let _,args = destApp (project gl') (EConstr.of_constr (pf_concl gl')) in
+	   let _,args = destApp (project gl') (pf_concl gl') in
 	   Array.last args
 	 in
 	 let body_info rec_hyps =
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d964002f9..ba01b3b04 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -493,7 +493,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
   in
   let _ = evd := sigma in 
   let l_schemes =
-    List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma) schemes
+    List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma %> EConstr.Unsafe.to_constr) schemes
   in
   let i = ref (-1) in
   let sorts =
@@ -671,7 +671,7 @@ let build_case_scheme fa =
       Indrec.build_case_analysis_scheme_default env sigma ind sf
   in
   let sigma = Sigma.to_evar_map sigma in
-  let scheme_type =  (Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme) in
+  let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
   let sorts =
     (fun (_,_,x) ->
        Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index fc5a287ae..fd2f4bbd3 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -504,6 +504,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		*)
 		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
 		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in
+                let rt_typ = EConstr.Unsafe.to_constr rt_typ in
 		let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
@@ -612,6 +613,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let v_res = build_entry_lc env funnames avoid v in
 	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
 	let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in
+	let v_type = EConstr.Unsafe.to_constr v_type in
 	let new_env =
 	  match n with
 	      Anonymous -> env
@@ -629,7 +631,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) (EConstr.of_constr b_as_constr) in
 	let (ind,_) =
-	  try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ)
+	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	  with Not_found ->
 	    user_err  (str "Cannot find the inductive associated to " ++
 			       Printer.pr_glob_constr b ++ str " in " ++
@@ -661,7 +663,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) (EConstr.of_constr b_as_constr) in
 	  let (ind,_) =
-	    try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ)
+	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	    with Not_found ->
 	      user_err  (str "Cannot find the inductive associated to " ++
 				 Printer.pr_glob_constr b ++ str " in " ++
@@ -706,7 +708,7 @@ and build_entry_lc_from_case env funname make_discr
 	let types =
 	  List.map (fun (case_arg,_) ->
 		      let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
-		      Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr case_arg_as_constr)
+		      EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr case_arg_as_constr))
 		   ) el
 	in
 	(****** The next works only if the match is not dependent ****)
@@ -755,6 +757,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			let typ_of_id =
 			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
 			in
+			let typ_of_id = EConstr.Unsafe.to_constr typ_of_id in
 			let raw_typ_of_id =
 			  Detyping.detype false []
 			    env_with_pat_ids (Evd.from_env env) typ_of_id
@@ -808,6 +811,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		      if Id.Set.mem id this_pat_ids
 		      then (Prod (Name id),
 		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
+		      let typ_of_id = EConstr.Unsafe.to_constr typ_of_id in
 		      let raw_typ_of_id =
 			Detyping.detype false [] new_env (Evd.from_env env) typ_of_id
 		      in
@@ -1122,6 +1126,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  let t',ctx = Pretyping.understand env evd t in
 	  let evd = Evd.from_ctx ctx in
 	  let type_t' = Typing.unsafe_type_of env evd (EConstr.of_constr t') in
+	  let type_t' = EConstr.Unsafe.to_constr type_t' in
 	  let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in
 	  let new_b,id_to_exclude =
 	    rebuild_cons new_env
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e22fed391..1cde4420e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -78,11 +78,11 @@ let functional_induction with_clean c princl pat =
 				     ++Printer.pr_leconstr (mkConst c') )
 	      in
 	      let princ = EConstr.of_constr princ in
-	      (princ,NoBindings,EConstr.of_constr (Tacmach.pf_unsafe_type_of g' princ),g')
+	      (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
 	   | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
 	 end
       | Some ((princ,binding)) ->
-	 princ,binding,EConstr.of_constr (Tacmach.pf_unsafe_type_of g princ),g
+	 princ,binding,Tacmach.pf_unsafe_type_of g princ,g
     in
     let sigma = Tacmach.project g' in
     let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index be82010d9..5cbec7743 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -263,7 +263,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     let princ_type =  nf_zeta 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
+    let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* Since we cannot ensure that the functional principle is defined in the
@@ -315,7 +315,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	List.fold_right 
 	  (fun hid acc ->
 	     let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
-	     let type_of_hid = EConstr.of_constr type_of_hid in
 	     let sigma = project g in
 	     match EConstr.kind sigma type_of_hid with
 	       | Prod(_,_,t') ->
@@ -503,7 +502,7 @@ and intros_with_rewrite_aux : tactic =
   fun g ->
     let eq_ind = make_eq () in
     let sigma = project g in
-    match EConstr.kind sigma (EConstr.of_constr (pf_concl g)) with
+    match EConstr.kind sigma (pf_concl g) with
 	  | Prod(_,t,t') ->
 	      begin
 		match EConstr.kind sigma t with
@@ -591,7 +590,7 @@ and intros_with_rewrite_aux : tactic =
 let rec reflexivity_with_destruct_cases g =
   let destruct_case () =
     try
-      match EConstr.kind (project g) (snd (destApp (project g) (EConstr.of_constr (pf_concl g)))).(2) with
+      match EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2) with
 	| Case(_,_,v,_) ->
 	    tclTHENSEQ[
 	      Proofview.V82.of_tactic (simplest_case v);
@@ -608,7 +607,7 @@ let rec reflexivity_with_destruct_cases g =
 	 match sc with
 	     None -> tclIDTAC g
 	   | Some id ->
-	       match EConstr.kind (project g) (EConstr.of_constr (pf_unsafe_type_of g (mkVar id))) with
+	       match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with
 		 | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
 		     if Equality.discriminable (pf_env g) (project g) t1 t2
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
@@ -674,12 +673,11 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     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 = 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
        and compute a fresh name for each of them
     *)
-    let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
+    let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* and fresh names for res H and the principle (cf bug bug #1174) *)
@@ -937,7 +935,6 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 let revert_graph kn post_tac hid g =
     let sigma = project g in
     let typ = pf_unsafe_type_of g (mkVar hid) in
-    let typ = EConstr.of_constr typ in
     match EConstr.kind sigma typ with
       | App(i,args) when isInd sigma i ->
 	  let ((kn',num) as ind'),u = destInd sigma i in
@@ -990,7 +987,6 @@ let functional_inversion kn hid fconst f_correct : tactic =
     let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
     let sigma = project g in
     let type_of_h = pf_unsafe_type_of g (mkVar hid) in
-    let type_of_h = EConstr.of_constr type_of_h in
     match EConstr.kind sigma type_of_h with
       | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ())  ->
 	  let pre_tac,f_args,res =
@@ -1044,7 +1040,6 @@ let invfun qhyp f g =
 	  (fun hid -> Proofview.V82.tactic begin fun g ->
             let sigma = project g in
 	     let hyp_typ = pf_unsafe_type_of g (mkVar hid)  in
-	     let hyp_typ = EConstr.of_constr hyp_typ in
 	     match EConstr.kind sigma hyp_typ with
 	       | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
 		   begin
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a80a7b5e7..adbdb1eb7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -123,7 +123,7 @@ let pf_get_new_ids idl g =
 
 let compute_renamed_type gls c =
   EConstr.of_constr (rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
-    (pf_unsafe_type_of gls c))
+    (EConstr.Unsafe.to_constr (pf_unsafe_type_of gls c)))
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
 let ano_id = Id.of_string "anonymous"
@@ -412,7 +412,6 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 	    h_intros to_intros;
 	    (fun g' -> 
 	      let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
-	      let ty_teq = EConstr.of_constr ty_teq in
 	      let teq_lhs,teq_rhs =
 		let _,args = try destApp (project g') ty_teq with DestKO -> assert false in
 		args.(1),args.(2)
@@ -522,19 +521,19 @@ let rec prove_lt hyple g =
   let sigma = project g in
   begin
     try
-      let (varx,varz) = match decompose_app sigma (EConstr.of_constr (pf_concl g)) with
+      let (varx,varz) = match decompose_app sigma (pf_concl g) with
         | _, x::z::_ when isVar sigma x && isVar sigma z -> x, z
         | _ -> assert false
       in
       let h =
 	List.find (fun id ->
-          match decompose_app sigma (EConstr.of_constr (pf_unsafe_type_of g (mkVar id))) with
+          match decompose_app sigma (pf_unsafe_type_of g (mkVar id)) with
             | _, t::_ -> EConstr.eq_constr sigma t varx
             | _ -> false
 	) hyple
       in
       let y =
-	List.hd (List.tl (snd (decompose_app sigma (EConstr.of_constr (pf_unsafe_type_of g (mkVar h)))))) in
+	List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (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)
@@ -698,7 +697,6 @@ let mkDestructEq :
         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 = EConstr.of_constr type_of_expr in
   let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
            to_revert_constr in
     pf_typel new_hyps (fun _ ->
@@ -707,7 +705,7 @@ let mkDestructEq :
       (fun g2 ->
         let changefun patvars = { run = fun sigma ->
           let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
-          let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2)) in
+          let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2) in
           Sigma (c, sigma, p)
         } in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
@@ -846,7 +844,7 @@ let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos =
 let rec prove_le g = 
   let sigma = project g in
   let x,z = 
-    let _,args = decompose_app sigma (EConstr.of_constr (pf_concl g)) in 
+    let _,args = decompose_app sigma (pf_concl g) in 
     (List.hd args,List.hd (List.tl args))
   in 
   tclFIRST[
@@ -857,9 +855,8 @@ let rec prove_le g =
 	let matching_fun = 
 	  pf_is_matching g
 	    (Pattern.PApp(Pattern.PRef (reference_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in 
-	let (h,t) = List.find (fun (_,t) -> matching_fun (EConstr.of_constr t)) (pf_hyps_types g)
+	let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g)
 	in 
-	let t = EConstr.of_constr t in
 	let y = 
 	  let _,args = decompose_app sigma t in 
 	  List.hd (List.tl args)
@@ -1350,7 +1347,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	     ] gls)
       (fun g ->
         let sigma = project g in
-	 match EConstr.kind sigma (EConstr.of_constr (pf_concl g)) with
+	 match EConstr.kind sigma (pf_concl g) with
 	   | App(f,_) when EConstr.eq_constr sigma f (well_founded ()) ->
 	       Proofview.V82.of_tactic (Auto.h_auto None [] (Some []))  g
 	   | _ ->
@@ -1523,9 +1520,11 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let env = Global.env() in
   let evd = ref (Evd.from_env env) in
   let function_type = interp_type_evars env evd type_of_f in
+  let function_type = EConstr.Unsafe.to_constr function_type in
   let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
   let ty = interp_type_evars env evd ~impls:rec_impls eq in
+  let ty = EConstr.Unsafe.to_constr ty in
   let evm, nf = Evarutil.nf_evars_and_universes !evd in
   let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in
   let function_type = nf function_type in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ced572466..a2346cc90 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1606,6 +1606,7 @@ let rec parse_hyps gl parse_arith env tg hyps =
  match hyps with
   | [] -> ([],env,tg)
   | (i,t)::l ->
+    let t = EConstr.Unsafe.to_constr t in
      let (lhyps,env,tg) = parse_hyps gl parse_arith env tg l in
       try
        let (c,env,tg) = parse_formula gl parse_arith env  tg t in
@@ -1713,7 +1714,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
        ("__varmap", vm, Term.mkApp( coq_VarMap, [|spec.typ|])); 
        ("__wit", cert, cert_typ)
       ]
-      (Tacmach.pf_concl gl))
+      (EConstr.Unsafe.to_constr (Tacmach.pf_concl gl)))
   ] 
   end }
 
@@ -1964,6 +1965,7 @@ let micromega_gen
  Proofview.Goal.nf_enter { enter = begin fun gl -> 
     let gl = Tacmach.New.of_old (fun x -> x) gl in
     let concl = Tacmach.pf_concl gl in
+    let concl = EConstr.Unsafe.to_constr concl in
     let hyps  = Tacmach.pf_hyps_types gl in
     try
      let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
@@ -2051,7 +2053,7 @@ let micromega_order_changer cert env ff  =
 	    [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|]));
          ("__wit", cert, cert_typ)
         ]
-        (Tacmach.pf_concl gl)));
+        (EConstr.Unsafe.to_constr (Tacmach.pf_concl gl))));
      (*      Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)*)
      ]
   end }
@@ -2072,6 +2074,7 @@ let micromega_genr prover tac =
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
      let gl = Tacmach.New.of_old (fun x -> x) gl in
      let concl = Tacmach.pf_concl gl in
+     let concl = EConstr.Unsafe.to_constr concl in
      let hyps  = Tacmach.pf_hyps_types gl in
 
      try
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 51790f4c9..665486272 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -38,9 +38,9 @@ open OmegaSolver
 
 let elim_id id =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-    simplest_elim (EConstr.of_constr (Tacmach.New.pf_global id gl))
+    simplest_elim (Tacmach.New.pf_global id gl)
   end }
-let resolve_id id gl = Proofview.V82.of_tactic (apply (EConstr.of_constr (pf_global gl id))) gl
+let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
 
 let timing timer_name f arg = f arg
 
@@ -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 -> EConstr.Unsafe.to_constr (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) (EConstr.Unsafe.to_constr (pf_concl gl)) in
   let newc = EConstr.of_constr newc in
   Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
 
@@ -632,6 +632,7 @@ let mkNewMeta () = mkMeta (Evarutil.new_meta())
 
 let clever_rewrite_base_poly typ p result theorem gl =
   let full = pf_concl gl in
+  let full = EConstr.Unsafe.to_constr full in
   let (abstracted,occ) = abstract_path typ (List.rev p) full in
   let t =
     applist
@@ -663,6 +664,7 @@ let clever_rewrite_gen_nat p result (t,args) =
 
 let clever_rewrite p vpath t gl =
   let full = pf_concl gl in
+  let full = EConstr.Unsafe.to_constr full in
   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
@@ -1424,6 +1426,7 @@ let coq_omega =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   clear_constr_tables ();
   let hyps_types = Tacmach.New.pf_hyps_types gl in
+  let hyps_types = List.map (on_snd EConstr.Unsafe.to_constr) hyps_types in
   let destructure_omega = Tacmach.New.of_old destructure_omega gl in
   let tactic_normalisation, system =
     List.fold_left destructure_omega ([],[]) hyps_types in
@@ -1607,6 +1610,7 @@ let nat_inject =
 	  with e when catchable_exception e -> loop lit end
   in
   let hyps_types = Tacmach.New.pf_hyps_types gl in
+  let hyps_types = List.map (on_snd EConstr.Unsafe.to_constr) hyps_types in
   loop (List.rev hyps_types)
   end }
 
@@ -1722,7 +1726,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 (EConstr.of_constr t2))
+              if is_Prop (EConstr.Unsafe.to_constr (type_of (EConstr.of_constr t2)))
               then
 		let d1 = decidability t1 in
 		Tacticals.New.tclTHENLIST [
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 87276f5df..edf34607b 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -459,8 +459,7 @@ let quote f lid =
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let f = Tacmach.New.pf_global f gl in
-    let f = EConstr.of_constr f in
-    let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
+    let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in
     let ivs = compute_ivs f cl gl in
     let concl = Proofview.Goal.concl gl in
     let quoted_terms = quote_terms env sigma ivs [concl] in
@@ -478,8 +477,7 @@ let gen_quote cont c f lid =
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let f = Tacmach.New.pf_global f gl in
-  let f = EConstr.of_constr f in
-  let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
+  let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in
   let ivs = compute_ivs f cl gl in
   let quoted_terms = quote_terms env sigma ivs [c] in
   let (p, vm) = match quoted_terms with
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index ab5033601..cfe14b230 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -740,6 +740,7 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c =
 
 let reify_gl env gl =
   let concl = Tacmach.pf_concl gl in
+  let concl = EConstr.Unsafe.to_constr concl in
   let t_concl =
     Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in
   if !debug then begin
@@ -748,6 +749,7 @@ let reify_gl env gl =
   end;
   let rec loop = function
       (i,t) :: lhyps ->
+        let t = EConstr.Unsafe.to_constr t in
 	let t' = oproposition_of_constr env (false,[],i,[]) gl t in
 	if !debug then begin
 	  Printf.printf "  %s: " (Names.Id.to_string i);
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 981ce2a61..475380512 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -262,8 +262,9 @@ let rtauto_tac gls=
   let gl=pf_concl gls in
   let _=
     if Retyping.get_sort_family_of
-      (pf_env gls) (Tacmach.project gls) (EConstr.of_constr gl) != InProp
+      (pf_env gls) (Tacmach.project gls) gl != InProp
     then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in
+  let gl = EConstr.Unsafe.to_constr gl in
   let glf=make_form gamma gls gl in
   let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in
   let formula=
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 358ea5685..f52557095 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -142,7 +142,7 @@ let ic c =
   let env = Global.env() in
   let sigma = Evd.from_env env in
   let sigma, c = Constrintern.interp_open_constr env sigma c in
-  (sigma, EConstr.of_constr c)
+  (sigma, c)
 
 let ic_unsafe c = (*FIXME remove *)
   let env = Global.env() in
@@ -505,8 +505,6 @@ let ring_equality env evd (r,add,mul,opp,req) =
             | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
 	let setoid = Typing.e_solve_evars env evd setoid in
 	let op_morph = Typing.e_solve_evars env evd op_morph in
-	let setoid = EConstr.of_constr setoid in
-	let op_morph = EConstr.of_constr op_morph in
 	  (setoid,op_morph)
     | _ ->
 	let setoid = setoid_of_relation (Global.env ()) evd r req in
@@ -594,6 +592,7 @@ let make_hyp_list env evd lH =
       (plapp evd coq_nil [|carrier|])
   in 
   let l' = Typing.e_solve_evars env evd l in
+  let l' = EConstr.Unsafe.to_constr l' in
     Evarutil.nf_evars_universes !evd l'
 
 let interp_power env evd pow =
@@ -756,7 +755,7 @@ let ring_lookup (f : Value.t) lH rl t =
       let rl = make_args_list sigma rl t in
       let evdref = ref sigma in
       let e = find_ring_structure env sigma rl in
-      let rl = carg (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
+      let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
       let lH = carg (make_hyp_list env evdref lH) in
       let ring = ltac_ring_structure e in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl]))
@@ -1039,7 +1038,7 @@ let field_lookup (f : Value.t) lH rl t =
       let rl = make_args_list sigma rl t in
       let evdref = ref sigma in
       let e = find_field_structure env sigma rl in
-      let rl = carg (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
+      let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
       let lH = carg (make_hyp_list env evdref lH) in
       let field = ltac_field_structure e in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl]))
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 9dcc6c4cc..eb5f401e3 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1353,6 +1353,7 @@ let fill_occ_term env cl occ sigma0 (sigma, t) =
 
 let pf_fill_occ_term gl occ t =
   let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in
+  let concl = EConstr.Unsafe.to_constr concl in
   let cl,(_,t) = fill_occ_term env concl occ sigma0 t in
   cl, t
 
@@ -1388,6 +1389,7 @@ let ssrpatterntac _ist (arg_ist,arg) gl =
   let pat = interp_rpattern arg_ist gl arg in
   let sigma0 = project gl in
   let concl0 = pf_concl gl in
+  let concl0 = EConstr.Unsafe.to_constr concl0 in
   let (t, uc), concl_x =
     fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in
   let t = EConstr.of_constr t in
@@ -1416,6 +1418,7 @@ let ssrinstancesof ist arg gl =
   let ok rhs lhs ise = true in
 (*   not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *)
   let env, sigma, concl = pf_env gl, project gl, pf_concl gl in
+  let concl = EConstr.Unsafe.to_constr concl in
   let sigma0, cpat = interp_cpattern ist gl arg None in
   let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in
   let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in