Removing various compatibility layers of tactics.

6 files changed, 40 insertions, 45 deletions

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