Typing API using EConstr.

31 files changed, 169 insertions, 147 deletions

diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml
index c5b26e6d5..5d3b2b886 100644
--- a/ltac/evar_tactics.ml
+++ b/ltac/evar_tactics.ml
@@ -77,7 +77,7 @@ let let_evar name typ =
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     let sigma = ref sigma in
-    let _ = Typing.e_sort_of env sigma typ in
+    let _ = Typing.e_sort_of env sigma (EConstr.of_constr typ) in
     let sigma = Sigma.Unsafe.of_evar_map !sigma in
     let id = match name with
     | Names.Anonymous -> 
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 076e4c05e..5703687c4 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -113,7 +113,7 @@ let extends_undefined evars evars' =
 let app_poly_check env evars f args =
   let (evars, cstrs), fc = f evars in
   let evdref = ref evars in 
-  let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in
+  let t = Typing.e_solve_evars env evdref (EConstr.of_constr (mkApp (fc, args))) in
     (!evdref, cstrs), t
 
 let app_poly_nocheck env evars f args =
@@ -382,7 +382,7 @@ end
 
 let type_app_poly env env evd f args =
   let evars, c = app_poly_nocheck env evd f args in
-  let evd', t = Typing.type_of env (goalevars evars) c in
+  let evd', t = Typing.type_of env (goalevars evars) (EConstr.of_constr c) in
     (evd', cstrevars evars), c
 
 module PropGlobal = struct
@@ -485,7 +485,7 @@ let rec decompose_app_rel env evd t =
   | App (f, [||]) -> assert false
   | App (f, [|arg|]) ->
     let (f', argl, argr) = decompose_app_rel env evd arg in
-    let ty = Typing.unsafe_type_of env evd argl in
+    let ty = Typing.unsafe_type_of env evd (EConstr.of_constr argl) in
     let f'' = mkLambda (Name default_dependent_ident, ty,
       mkLambda (Name (Id.of_string "y"), lift 1 ty,
         mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
@@ -787,7 +787,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
     let morphargs, morphobjs = Array.chop first args in
     let morphargs', morphobjs' = Array.chop first args' in
     let appm = mkApp(m, morphargs) in
-    let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in
+    let appmtype = Typing.unsafe_type_of env (goalevars evars) (EConstr.of_constr appm) in
     let cstrs = List.map 
       (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) 
       (Array.to_list morphobjs') 
@@ -1477,7 +1477,7 @@ type result = (evar_map * constr option * types) option option
 
 let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result =
   let evdref = ref sigma in
-  let sort = Typing.e_sort_of env evdref concl in
+  let sort = Typing.e_sort_of env evdref (EConstr.of_constr concl) in
   let evars = (!evdref, Evar.Set.empty) in
   let evars, cstr =
     let prop, (evars, arrow) = 
@@ -1870,7 +1870,7 @@ let declare_projection n instance_id r =
   let sigma,c = Evd.fresh_global env sigma r in
   let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in
   let term = proper_projection c ty in
-  let sigma, typ = Typing.type_of env sigma term in
+  let sigma, typ = Typing.type_of env sigma (EConstr.of_constr term) in
   let ctx, typ = decompose_prod_assum typ in
   let typ =
     let n =
@@ -1902,7 +1902,7 @@ let declare_projection n instance_id r =
 let build_morphism_signature env sigma m =
   let m,ctx = Constrintern.interp_constr env sigma m in
   let sigma = Evd.from_ctx ctx in
-  let t = Typing.unsafe_type_of env sigma m in
+  let t = Typing.unsafe_type_of env sigma (EConstr.of_constr m) in
   let cstrs =
     let rec aux t =
       match kind_of_term t with
@@ -1932,7 +1932,7 @@ let build_morphism_signature env sigma m =
 let default_morphism sign m =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let t = Typing.unsafe_type_of env sigma m in
+  let t = Typing.unsafe_type_of env sigma (EConstr.of_constr m) in
   let evars, _, sign, cstrs =
     PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
   in
@@ -2126,7 +2126,7 @@ let setoid_proof ty fn fallback =
       begin
         try
           let rel, _, _ = decompose_app_rel env sigma concl in
-          let (sigma, t) = Typing.type_of env sigma rel in
+          let (sigma, t) = Typing.type_of env sigma (EConstr.of_constr rel) in
           let car = RelDecl.get_type (List.hd (fst (Reduction.dest_prod env t))) in
 	    (try init_relation_classes () with _ -> raise Not_found);
             fn env sigma car rel
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 34faa028f..8f5ac7e76 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -791,7 +791,7 @@ let interp_may_eval f ist env sigma = function
 	let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
 	let evdref = ref sigma in
 	let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
-	let c = Typing.e_solve_evars env evdref c in
+	let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
 	!evdref , c
       with
 	| Not_found ->
@@ -799,7 +799,7 @@ let interp_may_eval f ist env sigma = function
 	    (str "Unbound context identifier" ++ pr_id s ++ str"."))
   | ConstrTypeOf c ->
       let (sigma,c_interp) = f ist env sigma c in
-      Typing.type_of ~refresh:true env sigma c_interp
+      Typing.type_of ~refresh:true env sigma (EConstr.of_constr c_interp)
   | ConstrTerm c ->
      try
 	f ist env sigma c
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 36a96fdb5..58454eedf 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -50,7 +50,7 @@ let whd_delta env=
 (* decompose member of equality in an applicative format *)
 
 (** FIXME: evar leak *)
-let sf_of env sigma c = e_sort_of env (ref sigma) c
+let sf_of env sigma c = e_sort_of env (ref sigma) (EConstr.of_constr c)
 
 let rec decompose_term env sigma t=
     match kind_of_term (whd env t) with
@@ -247,7 +247,7 @@ let new_refine c = Proofview.V82.tactic (refine c)
 
 let assert_before n c =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let evm, _ = Tacmach.New.pf_apply type_of gl c in
+    let evm, _ = Tacmach.New.pf_apply type_of gl (EConstr.of_constr c) in
       Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
   end }
 
@@ -340,7 +340,7 @@ let refute_tac c t1 t2 p =
   end }
 
 let refine_exact_check c gl =
-  let evm, _ = pf_apply type_of gl c in
+  let evm, _ = pf_apply type_of gl (EConstr.of_constr c) in
     Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
 
 let convert_to_goal_tac c t1 t2 p = 
@@ -480,10 +480,10 @@ let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
   Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
-    let evm, ty = pf_apply type_of gl c1 in
+    let evm, ty = pf_apply type_of gl (EConstr.of_constr c1) in
     let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm (EConstr.of_constr ty) in
     let term = mkApp (fc, [| ty; c1; c2 |]) in
-    let evm, _ =  type_of (pf_env gl) evm term in
+    let evm, _ =  type_of (pf_env gl) evm (EConstr.of_constr term) in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
 			  (k term)
     end })
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c17c8dbb8..dcebf7806 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -429,7 +429,7 @@ 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) concl) in
+  let sort = family_of_sort (Typing.e_sort_of env (ref evd) (EConstr.of_constr concl)) in
   let rec aux env avoid subst = function
       [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
     | (n,typ)::rest ->
@@ -437,7 +437,7 @@ let concl_refiner metas body gls =
 	let x = id_of_name_using_hdchar env _A Anonymous in
 	let _x = fresh_id avoid x gls in
 	let nenv = Environ.push_named (LocalAssum (_x,_A)) env in
-	let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) _A) in
+	let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) (EConstr.of_constr _A)) in
 	let nsubst = (n,mkVar _x)::subst in
 	  if List.is_empty rest then
 	    asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a3513692c..44bdb585a 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -155,7 +155,7 @@ let left_instance_tac (inst,id) continue seq=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
 		  let evmap, _ =
-		    try Typing.type_of (pf_env gl) evmap gt
+		    try Typing.type_of (pf_env gl) evmap (EConstr.of_constr gt)
 		    with e when CErrors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
 		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 340dd2c28..0a7938069 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -329,7 +329,7 @@ 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 to_refine in
+	   let evm, _ = pf_apply Typing.type_of g (EConstr.of_constr to_refine) in
 	     tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g
 	)
     in
@@ -544,7 +544,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
       tclIDTAC
   in
   try
-    scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id]
+    scan_type [] (Typing.unsafe_type_of env sigma (EConstr.mkVar hyp_id)), [hyp_id]
   with TOREMOVE ->
     thin [hyp_id],[]
 
@@ -639,7 +639,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 	fun g ->
 	  let prov_hid = pf_get_new_id hid g in
 	  let c = mkApp(mkVar hid,args) in
-	  let evm, _ = pf_apply Typing.type_of g c in
+	  let evm, _ = pf_apply Typing.type_of g (EConstr.of_constr c) in
 	  tclTHENLIST[
             Refiner.tclEVARS evm;
 	    Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
@@ -968,7 +968,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
   (*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
   let (type_ctxt,type_of_f),evd =
-    let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f
+    let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f)
     in 
     decompose_prod_n_assum
       (nb_params + nb_args) t,evd
@@ -1039,7 +1039,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 	  (Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
       in
       evd:=evd';                       
-      let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in 
+      let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr res) in 
       res
   in
   let nb_intro_to_do = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9637632a6..4b47b83af 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -283,7 +283,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   let new_princ_name =
     next_ident_away_in_goal (Id.of_string "___________princ_________") []
   in
-  let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in
+  let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in
   let hook = Lemmas.mk_hook (hook new_principle_type) in
   begin
     Lemmas.start_proof
@@ -337,7 +337,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
 	let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
 	let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
-	let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in
+	let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
 	(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
 	let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in
 	ignore(
@@ -488,7 +488,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
   in
   let _ = evd := sigma in 
   let l_schemes =
-    List.map (Typing.unsafe_type_of env sigma) schemes
+    List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma) schemes
   in
   let i = ref (-1) in
   let sorts =
@@ -616,7 +616,7 @@ let build_scheme fas =
 	    in
 	    let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
             let _ = evd := evd' in 
-	    let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in 
+	    let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in 
 	    (destConst f,sort)
 	 )
 	 fas
@@ -666,7 +666,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 ) scheme in
+  let scheme_type =  (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 92de4d873..38cd21684 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -503,7 +503,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		   The "value" of this branch is then simply [res]
 		*)
 		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) rt_as_constr in
+		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) 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
@@ -611,7 +611,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) v_as_constr in
+	let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in
 	let new_env =
 	  match n with
 	      Anonymous -> env
@@ -627,7 +627,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	build_entry_lc_from_case env funnames make_discr el brl avoid
     | GIf(_,b,(na,e_option),lhs,rhs) ->
 	let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
-	let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
+	let 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)
 	  with Not_found ->
@@ -659,7 +659,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	      nal
 	  in
 	  let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
-	  let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
+	  let 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)
 	    with Not_found ->
@@ -706,7 +706,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) case_arg_as_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 ****)
@@ -753,7 +753,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		   List.fold_right
 		     (fun id acc ->
 			let typ_of_id =
-			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (mkVar id)
+			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
 			in
 			let raw_typ_of_id =
 			  Detyping.detype false []
@@ -807,7 +807,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		   (fun id  acc ->
 		      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) (mkVar id) in
+		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
 		      let raw_typ_of_id =
 			Detyping.detype false [] new_env (Evd.from_env env) typ_of_id
 		      in
@@ -1121,7 +1121,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  let evd = (Evd.from_env env) in
 	  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 t' in
+	  let type_t' = Typing.unsafe_type_of env evd (EConstr.of_constr 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
@@ -1272,7 +1272,7 @@ let do_build_inductive
   let evd,env =
     Array.fold_right2
       (fun id c (evd,env) ->
-       let evd,t = Typing.type_of env evd (mkConstU c) in
+       let evd,t = Typing.type_of env evd (EConstr.mkConstU c) in
        evd,
        Environ.push_named (LocalAssum (id,t))
 			   (* try *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a264c37c5..0743fc5d9 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -369,7 +369,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	     let evd = ref (Evd.from_env env) in
 	     let evd',uprinc = Evd.fresh_global env !evd princ in
              let _ = evd := evd' in 
-	     let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in
+	     let princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in
     	     Functional_principles_types.generate_functional_principle
 	       evd
 		 interactive_proof
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 9abe60402..e5286fb1f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -134,7 +134,7 @@ let generate_type evd g_to_f f graph i =
     Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd graph)))
   in
   evd:=evd';
-  let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
+  let graph_arity = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr graph) in
   let ctxt,_ = decompose_prod_assum graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
@@ -202,7 +202,7 @@ let find_induction_principle evd f =
     | None -> raise Not_found
     | Some rect_lemma ->
        let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (Globnames.ConstRef rect_lemma) in
-       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
+       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr rect_lemma) in
        evd:=evd';
        rect_lemma,typ
 
@@ -449,7 +449,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	     "functional_induction" (
 	       (fun gl ->
 		let term = mkApp (mkVar principle_id,Array.of_list bindings) in
-		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl term in
+		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl (EConstr.of_constr term) in
 		Proofview.V82.of_tactic (apply term) gl')
 	   ))
 	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
@@ -792,7 +792,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
 	 let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
-	 let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in 
+	 let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in 
 	   let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
 	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 4fd9e0ff8..12ed758ba 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -657,7 +657,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
   continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} 
 
 let pf_type c tac gl = 
-  let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
+  let evars, ty = Typing.type_of (pf_env gl) (project gl) (EConstr.of_constr c) in
     tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
 
 let pf_typel l tac =
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e1b95ddbc..b0a3e839b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -493,8 +493,8 @@ let ring_equality env evd (r,add,mul,opp,req) =
 	  match opp with
               Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
             | 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 = Typing.e_solve_evars env evd (EConstr.of_constr setoid) in
+	let op_morph = Typing.e_solve_evars env evd (EConstr.of_constr op_morph) in
 	  (setoid,op_morph)
     | _ ->
 	let setoid = setoid_of_relation (Global.env ()) evd r req in
@@ -581,7 +581,7 @@ let make_hyp_list env evd lH =
       (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
       (plapp evd coq_nil [|carrier|])
   in 
-  let l' = Typing.e_solve_evars env evd l in
+  let l' = Typing.e_solve_evars env evd (EConstr.of_constr l) in
     Evarutil.nf_evars_universes !evd l'
 
 let interp_power env evd pow =
@@ -707,7 +707,7 @@ let make_term_list env evd carrier rl =
   let l = List.fold_right
     (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
     (plapp evd coq_nil [|carrier|])
-  in Typing.e_solve_evars env evd l
+  in Typing.e_solve_evars env evd (EConstr.of_constr l)
 
 let carg = Tacinterp.Value.of_constr
 let tacarg expr =
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 04f50d50e..882c052f6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1381,7 +1381,7 @@ and match_current pb (initial,tomatch) =
 	  let case =
 	    make_case_or_project pb.env indf ci pred current brvals
 	  in
-	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
+	  Typing.check_allowed_sort pb.env !(pb.evdref) mind (EConstr.of_constr current) (EConstr.of_constr pred);
 	  { uj_val = applist (case, inst);
 	    uj_type = prod_applist typ inst }
 
@@ -1684,7 +1684,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
 	(lift (n'-n) impossible_case_type, mkSort u)
     | Some t ->
         let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
-        let evd,tt = Typing.type_of extenv !evdref t in
+        let evd,tt = Typing.type_of extenv !evdref (EConstr.of_constr t) in
         evdref := evd;
         (t,tt) in
   let b = e_cumul env evdref (EConstr.of_constr tt) (EConstr.mkSort s) (* side effect *) in
@@ -1920,7 +1920,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   assert (len == 0);
   let p = predicate 0 c in
   let env' = List.fold_right push_rel_context arsign env in
-  try let sigma' = fst (Typing.type_of env' sigma p) in
+  try let sigma' = fst (Typing.type_of env' sigma (EConstr.of_constr p)) in
         Some (sigma', p)
   with e when precatchable_exception e -> None
 
@@ -2041,7 +2041,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	let IndType (indf, _) = 
 	  try find_rectype env ( !evdref) (EConstr.of_constr (lift (-(List.length realargs)) ty))
 	  with Not_found -> error_case_not_inductive env !evdref
-	    {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty}
+	    {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref (EConstr.of_constr ty)}
 	in
 	let (ind,u), params = dest_ind_family indf in
 	if not (eq_ind ind cind) then error_bad_constructor ~loc:l env cstr ind;
@@ -2242,7 +2242,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 let j = typing_fun (mk_tycon (EConstr.of_constr tycon)) rhs_env eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
-	 let _btype = evd_comb1 (Typing.type_of env) evdref bbody in
+	 let _btype = evd_comb1 (Typing.type_of env) evdref (EConstr.of_constr bbody) in
 	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in
 	 let branch =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0ea6758a7..04e235cc5 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -188,7 +188,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		  aux (hdy :: tele) (subst1 hdx restT) 
 		    (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
 	else Some (fun x -> 
-	  let term = co x in
+	  let term = EConstr.of_constr (co x) in
 	    Typing.e_solve_evars env evdref term)
       in
 	if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then
@@ -297,16 +297,16 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		   let evm = !evdref in
 		     (try subco ()
 		      with NoSubtacCoercion ->
-			let typ = Typing.unsafe_type_of env evm c in
-			let typ' = Typing.unsafe_type_of env evm c' in
+			let typ = Typing.unsafe_type_of env evm (EConstr.of_constr c) in
+			let typ' = Typing.unsafe_type_of env evm (EConstr.of_constr c') in
 			  coerce_application typ typ' c c' l l')
 		 else
 		   subco ()
 	   | x, y when Constr.equal c c' ->
 	       if Int.equal (Array.length l) (Array.length l') then
 		 let evm =  !evdref in
-		 let lam_type = Typing.unsafe_type_of env evm c in
-		 let lam_type' = Typing.unsafe_type_of env evm c' in
+		 let lam_type = Typing.unsafe_type_of env evm (EConstr.of_constr c) in
+		 let lam_type' = Typing.unsafe_type_of env evm (EConstr.of_constr c') in
 		   coerce_application lam_type lam_type' c c' l l'
 	       else subco ()
 	   | _ -> subco ())
@@ -337,7 +337,7 @@ let app_coercion env evdref coercion v =
   match coercion with
   | None -> v
   | Some f ->
-     let v' = Typing.e_solve_evars env evdref (f v) in
+     let v' = Typing.e_solve_evars env evdref (EConstr.of_constr (f v)) in
      whd_betaiota !evdref (EConstr.of_constr v')
 
 let coerce_itf loc env evd v t c1 =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 570f95324..28ba60812 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -507,7 +507,7 @@ let pretype_ref loc evdref env ref us =
   | ref ->
     let evd, c = pretype_global loc univ_flexible env !evdref ref us in
     let () = evdref := evd in
-    let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in
+    let ty = Typing.unsafe_type_of env.ExtraEnv.env evd (EConstr.of_constr c) in
       make_judge c ty
 
 let judge_of_Type loc evd s =
@@ -644,7 +644,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
 	      uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
         ctxtv vdef in
-      Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj;
+      Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names (Array.map EConstr.of_constr ftys) vdefj;
       let ftys = Array.map (nf_evar !evdref) ftys in
       let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
       let fixj = match fixkind with
@@ -898,7 +898,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    let fj = pretype (mk_tycon (EConstr.of_constr fty)) env_f evdref lvar d in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
-		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
+		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p);
 		obj ind p cj.uj_val fj.uj_val
 	    in
 	      { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
@@ -917,7 +917,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
-		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
+		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p);
 		obj ind p cj.uj_val fj.uj_val
 	    in { uj_val = v; uj_type = ccl })
 
@@ -981,7 +981,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let ind,_ = dest_ind_family indf in
 	let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in
 	let pred = nf_evar !evdref pred in
-	  Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred;
+	  Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr pred);
 	  mkCase (ci, pred, cj.uj_val, [|b1;b2|])
       in
       let cj = { uj_val = v; uj_type = p } in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 290d77b1b..a3983737d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1164,7 +1164,7 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
   let sigma = Sigma.to_evar_map sigma in
   let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (EConstr.Unsafe.to_constr c,sigma) in
   try
-    let _ = Typing.unsafe_type_of env sigma abstr_trm in
+    let _ = Typing.unsafe_type_of env sigma (EConstr.of_constr abstr_trm) in
     Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma)
   with Type_errors.TypeError (env',t) ->
     raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 64264cf08..c948f9b9a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -20,6 +20,11 @@ open Typeops
 open Arguments_renaming
 open Context.Rel.Declaration
 
+let push_rec_types pfix env =
+  let (i, c, t) = pfix in
+  let inj c = EConstr.Unsafe.to_constr c in
+  push_rec_types (i, Array.map inj c, Array.map inj t) env
+
 let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv
@@ -28,12 +33,12 @@ let meta_type evd mv =
 
 let constant_type_knowing_parameters env cst jl =
   let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
-  type_of_constant_knowing_parameters_in env cst paramstyp
+  EConstr.of_constr (type_of_constant_knowing_parameters_in env cst paramstyp)
 
 let inductive_type_knowing_parameters env (ind,u) jl =
   let mspec = lookup_mind_specif env ind in
   let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
-  Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
+  EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
 
 let e_type_judgment env evdref j =
   match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref (EConstr.of_constr j.uj_type))) with
@@ -44,7 +49,7 @@ let e_type_judgment env evdref j =
     | _ -> error_not_type env j
 
 let e_assumption_of_judgment env evdref j =
-  try (e_type_judgment env evdref j).utj_val
+  try EConstr.of_constr (e_type_judgment env evdref j).utj_val
   with TypeError _ ->
     error_assumption env j
 
@@ -84,27 +89,28 @@ let max_sort l =
   if Sorts.List.mem InSet l then InSet else InProp
 
 let e_is_correct_arity env evdref c pj ind specif params =
+  let open EConstr in
   let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
   let allowed_sorts = elim_sorts specif in
   let error () = error_elim_arity env ind allowed_sorts c pj None in
   let rec srec env pt ar =
-    let pt' = whd_all env !evdref (EConstr.of_constr pt) in
-    match kind_of_term pt', ar with
+    let pt' = EConstr.of_constr (whd_all env !evdref pt) in
+    match EConstr.kind !evdref pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
-        if not (Evarconv.e_cumul env evdref (EConstr.of_constr a1) (EConstr.of_constr a1')) then error ();
-        srec (push_rel (LocalAssum (na1,a1)) env) t ar'
+        if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error ();
+        srec (push_rel (LocalAssum (na1,EConstr.Unsafe.to_constr a1)) env) t ar'
     | Sort s, [] ->
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
         then error ()
     | Evar (ev,_), [] ->
         let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in
-        evdref := Evd.define ev (mkSort s) evd
+        evdref := Evd.define ev (Constr.mkSort s) evd
     | _, (LocalDef _ as d)::ar' ->
-        srec (push_rel d env) (lift 1 pt') ar'
+        srec (push_rel d env) (Vars.lift 1 pt') ar'
     | _ ->
         error ()
   in
-  srec env pj.uj_type (List.rev arsign)
+  srec env (EConstr.of_constr pj.uj_type) (List.rev arsign)
 
 let e_type_case_branches env evdref (ind,largs) pj c =
   let specif = lookup_mind_specif env (fst ind) in
@@ -128,24 +134,25 @@ let e_judge_of_case env evdref ci pj cj lfj =
     uj_type = rslty }
 
 let check_type_fixpoint loc env evdref lna lar vdefj =
+  let open EConstr in
   let lt = Array.length vdefj in
     if Int.equal (Array.length lar) lt then
       for i = 0 to lt-1 do
         if not (Evarconv.e_cumul env evdref (EConstr.of_constr (vdefj.(i)).uj_type)
-		  (EConstr.of_constr (lift lt lar.(i)))) then
+		  (Vars.lift lt lar.(i))) then
           Pretype_errors.error_ill_typed_rec_body ~loc env !evdref
-            i lna vdefj lar
+            i lna vdefj (Array.map EConstr.Unsafe.to_constr lar)
       done
 
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
-  let pj = Retyping.get_judgment_of env sigma (EConstr.of_constr p) in
+  let pj = Retyping.get_judgment_of env sigma p in
   let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
   if not (List.exists ((==) ksort) sorts) then
     let s = inductive_sort_family (snd specif) in
-    error_elim_arity env ind sorts c pj
+    error_elim_arity env ind sorts (EConstr.Unsafe.to_constr c) pj
       (Some(ksort,s,error_elim_explain ksort s))
 
 let e_judge_of_cast env evdref cj k tj =
@@ -160,21 +167,36 @@ let enrich_env env evdref =
   let penv' = Pre_env.({ penv with env_stratification =
     { penv.env_stratification with env_universes = Evd.universes !evdref } }) in
   Environ.env_of_pre_env penv'
+
+let check_fix env sigma pfix =
+  let inj c = EConstr.to_constr sigma c in
+  let (idx, (ids, cs, ts)) = pfix in
+  check_fix env (idx, (ids, Array.map inj cs, Array.map inj ts))
+
+let check_cofix env sigma pcofix =
+  let inj c = EConstr.to_constr sigma c in
+  let (idx, (ids, cs, ts)) = pcofix in
+  check_cofix env (idx, (ids, Array.map inj cs, Array.map inj ts))
+
+let make_judge c ty =
+  make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr ty)
 			  
 (* The typing machine with universes and existential variables. *)
 
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env evdref cstr =
-  match kind_of_term cstr with
+  let open EConstr in
+  let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
+  match EConstr.kind !evdref cstr with
     | Meta n ->
-        { uj_val = cstr; uj_type = meta_type !evdref n }
+        { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = meta_type !evdref n }
 
     | Evar ev ->
-	let ty = Evd.existential_type !evdref ev in
-	let jty = execute env evdref (whd_evar !evdref ty) in
+	let ty = EConstr.existential_type !evdref ev in
+	let jty = execute env evdref ty in
 	let jty = e_assumption_of_judgment env evdref jty in
-	{ uj_val = cstr; uj_type = jty }
+	{ uj_val = EConstr.Unsafe.to_constr cstr; uj_type = EConstr.Unsafe.to_constr jty }
 
     | Rel n ->
 	judge_of_relative env n
@@ -183,13 +205,13 @@ let rec execute env evdref cstr =
         judge_of_variable env id
 
     | Const c ->
-        make_judge cstr (rename_type_of_constant env c)
+        make_judge cstr (EConstr.of_constr (rename_type_of_constant env c))
 
     | Ind ind ->
-	make_judge cstr (rename_type_of_inductive env ind)
+	make_judge cstr (EConstr.of_constr (rename_type_of_inductive env ind))
 
     | Construct cstruct ->
-	make_judge cstr (rename_type_of_constructor env cstruct)
+	make_judge cstr (EConstr.of_constr (rename_type_of_constructor env cstruct))
 
     | Case (ci,p,c,lf) ->
         let cj = execute env evdref c in
@@ -200,13 +222,13 @@ let rec execute env evdref cstr =
     | Fix ((vn,i as vni),recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
 	let fix = (vni,recdef') in
-        check_fix env fix;
+        check_fix env !evdref fix;
 	make_judge (mkFix fix) tys.(i)
 
     | CoFix (i,recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
         let cofix = (i,recdef') in
-        check_cofix env cofix;
+        check_cofix env !evdref cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 
     | Sort (Prop c) ->
@@ -222,7 +244,7 @@ let rec execute env evdref cstr =
     | App (f,args) ->
         let jl = execute_array env evdref args in
 	let j =
-	  match kind_of_term f with
+	  match EConstr.kind !evdref f with
 	    | Ind ind when Environ.template_polymorphic_pind ind env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
@@ -273,7 +295,7 @@ and execute_recdef env evdref (names,lar,vdef) =
   let lara = Array.map (e_assumption_of_judgment env evdref) larj in
   let env1 = push_rec_types (names,lara,vdef) env in
   let vdefj = execute_array env1 evdref vdef in
-  let vdefv = Array.map j_val vdefj in
+  let vdefv = Array.map (j_val %> EConstr.of_constr) vdefj in
   let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in
   (names,lara,vdefv)
 
@@ -282,8 +304,8 @@ and execute_array env evdref = Array.map (execute env evdref)
 let e_check env evdref c t =
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-  if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) (EConstr.of_constr t)) then
-    error_actual_type env j (nf_evar !evdref t)
+  if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) t) then
+    error_actual_type env j (EConstr.to_constr !evdref t)
 
 (* Type of a constr *)
 
@@ -328,4 +350,4 @@ let e_solve_evars env evdref c =
   (* side-effect on evdref *)
   nf_evar !evdref c
 
-let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref (EConstr.Unsafe.to_constr c)))
+let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c))
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 04e5e40bc..3c1c4324d 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -14,33 +14,33 @@ open Evd
     and universes. *)
 
 (** Typecheck a term and return its type. May trigger an evarmap leak. *)
-val unsafe_type_of : env -> evar_map -> constr -> types
+val unsafe_type_of : env -> evar_map -> EConstr.constr -> types
 
 (** Typecheck a term and return its type + updated evars, optionally refreshing
     universes *)
-val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
+val type_of : ?refresh:bool -> env -> evar_map -> EConstr.constr -> evar_map * types
 
 (** Variant of [type_of] using references instead of state-passing. *)
-val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
+val e_type_of : ?refresh:bool -> env -> evar_map ref -> EConstr.constr -> types
 
 (** Typecheck a type and return its sort *)
-val e_sort_of : env -> evar_map ref -> types -> sorts
+val e_sort_of : env -> evar_map ref -> EConstr.types -> sorts
 
 (** Typecheck a term has a given type (assuming the type is OK) *)
-val e_check   : env -> evar_map ref -> constr -> types -> unit
+val e_check   : env -> evar_map ref -> EConstr.constr -> EConstr.types -> unit
 
 (** Returns the instantiated type of a metavariable *)
 val meta_type : evar_map -> metavariable -> types
 
 (** Solve existential variables using typing *)
-val e_solve_evars : env -> evar_map ref -> constr -> constr
+val e_solve_evars : env -> evar_map ref -> EConstr.constr -> constr
 
 (** Raise an error message if incorrect elimination for this inductive *)
 (** (first constr is term to match, second is return predicate) *)
-val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr ->
+val check_allowed_sort : env -> evar_map -> pinductive -> EConstr.constr -> EConstr.constr ->
   unit
 
 (** Raise an error message if bodies have types not unifiable with the
     expected ones *)
 val check_type_fixpoint : Loc.t -> env -> evar_map ref ->
-  Names.Name.t array -> types array -> unsafe_judgment array -> unit
+  Names.Name.t array -> EConstr.types array -> unsafe_judgment array -> unit
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ac2f14051..f418dc6a9 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -102,7 +102,7 @@ let abstract_list_all env evd typ c l =
   let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in
   let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in
   let evd,typp =
-    try Typing.type_of env evd p
+    try Typing.type_of env evd (EConstr.of_constr p)
     with
     | UserError _ ->
         error_cannot_find_well_typed_abstraction env evd p (List.map EConstr.of_constr l) None
@@ -1214,7 +1214,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
       | _ -> error "Apply_Head_Then"
   in
-    apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd
+    apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) (EConstr.of_constr c)) Sigma.refl evd
 
 let is_mimick_head ts f =
   match kind_of_term f with
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f4ac094b8..c2130a64a 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -29,7 +29,7 @@ open Sigma.Notations
 (* Abbreviations *)
 
 let pf_env = Refiner.pf_env
-let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma c
+let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma (EConstr.of_constr c)
 
 (******************************************************************)
 (* Clausal environments *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2df626e1c..93b31ced1 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -86,7 +86,7 @@ let apply_to_hyp check sign id f =
     else sign
 
 let check_typability env sigma c =
-  if !check then let _ = unsafe_type_of env sigma c in ()
+  if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in ()
 
 (************************************************************************)
 (************************************************************************)
@@ -330,7 +330,7 @@ let meta_free_prefix sigma a =
   with Stop acc -> Array.rev_of_list acc
 
 let goal_type_of env sigma c =
-  if !check then unsafe_type_of env sigma c
+  if !check then unsafe_type_of env sigma (EConstr.of_constr c)
   else Retyping.get_type_of env sigma (EConstr.of_constr c)
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
diff --git a/proofs/refine.ml b/proofs/refine.ml
index e6e3ef47d..b62f0bea4 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -28,12 +28,12 @@ let typecheck_evar ev env sigma =
   let info = Evd.find sigma ev in
   (** Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
-    let t = NamedDecl.get_type decl in
+    let t = EConstr.of_constr (NamedDecl.get_type decl) in
     let evdref = ref sigma in
     let _ = Typing.e_sort_of env evdref t in
     let () = match decl with
     | LocalAssum _ -> ()
-    | LocalDef (_,body,_) -> Typing.e_check env evdref body t
+    | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t
     in
     (!evdref, Environ.push_named decl env)
   in
@@ -42,12 +42,12 @@ let typecheck_evar ev env sigma =
   let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
   (** Typecheck the conclusion *)
   let evdref = ref sigma in
-  let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
+  let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in
   !evdref
 
 let typecheck_proof c concl env sigma =
   let evdref = ref sigma in
-  let () = Typing.e_check env evdref c concl in
+  let () = Typing.e_check env evdref (EConstr.of_constr c) (EConstr.of_constr concl) in
   !evdref
 
 let (pr_constrv,pr_constr) =
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b63b2ce28..148f9d675 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -93,8 +93,8 @@ 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_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
@@ -175,10 +175,10 @@ module New = struct
   let pf_concl = Proofview.Goal.concl
 
   let pf_unsafe_type_of gl t =
-    pf_apply unsafe_type_of gl t
+    pf_apply unsafe_type_of gl (EConstr.of_constr t)
 
   let pf_type_of gl t =
-    pf_apply type_of gl t
+    pf_apply type_of gl (EConstr.of_constr t)
 
   let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 46600cdd7..80b9ec06e 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -272,7 +272,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
       try
 	let others,(c1,c2) = split_last_two args in
 	let ty1, ty2 =
-	  Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2
+	  Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2)
 	in
 (* 	  if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
 (* 	  else *)
@@ -290,7 +290,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
 	| None -> None
 
 let find_applied_relation metas loc env sigma c left2right =
-  let ctype = Typing.unsafe_type_of env sigma c in
+  let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in
     match decompose_applied_relation metas env sigma c ctype left2right with
     | Some c -> c
     | None ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 17038e42d..58c86ff42 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1085,7 +1085,7 @@ let find_sigma_data env s = build_sigma_type ()
 let make_tuple env sigma (rterm,rty) lind =
   assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty)));
   let sigdata = find_sigma_data env (get_sort_of env sigma (EConstr.of_constr rty)) in
-  let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
+  let sigma, a = type_of ~refresh:true env sigma (EConstr.mkRel lind) in
   let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
   let rty = lift (1-lind) (liftn lind (lind+1) rty) in
@@ -1119,7 +1119,7 @@ let minimal_free_rels_rec env sigma =
   let rec minimalrec_free_rels_rec prev_rels (c,cty) =
     let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
     let combined_rels = Int.Set.union prev_rels direct_rels in
-    let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i)))
+    let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (EConstr.mkRel i)))
     in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
   in minimalrec_free_rels_rec Int.Set.empty
 
@@ -1165,7 +1165,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let rec sigrec_clausal_form siglen p_i =
     if Int.equal siglen 0 then
       (* is the default value typable with the expected type *)
-      let dflt_typ = unsafe_type_of env sigma dflt in
+      let dflt_typ = unsafe_type_of env sigma (EConstr.of_constr dflt) in
       try
 	let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) (EConstr.of_constr p_i) !evdref in
 	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
@@ -1184,7 +1184,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
           (destEvar ev)
       with
 	| Some w ->
-            let w_type = unsafe_type_of env sigma w in
+            let w_type = unsafe_type_of env sigma (EConstr.of_constr w) in
             if Evarconv.e_cumul env evdref (EConstr.of_constr w_type) (EConstr.of_constr a) then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
@@ -1273,7 +1273,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
     sigma, (tuple,tuplety,dfltval)
 
 let rec build_injrec env sigma dflt c = function
-  | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c)
+  | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma (EConstr.of_constr c))
   | ((sp,cnum),argnum)::l ->
     try
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1367,7 +1367,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       let injfun = mkNamedLambda e t injbody in
       let sigma,congr = Evd.fresh_global env sigma eq.congr in
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
-      let sigma, pf_typ = Typing.type_of env sigma pf in
+      let sigma, pf_typ = Typing.type_of env sigma (EConstr.of_constr pf) in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
       let pf = Clenvtac.clenv_value_cast_meta inj_clause in
       let ty = simplify_args env sigma (clenv_type inj_clause) in
@@ -1555,8 +1555,8 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
   let expected_goal = nf_betaiota sigma (EConstr.of_constr expected_goal) in
   (* Retype to get universes right *)
-  let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
-  let sigma, _ = Typing.type_of env sigma body in
+  let sigma, expected_goal_ty = Typing.type_of env sigma (EConstr.of_constr expected_goal) in
+  let sigma, _ = Typing.type_of env sigma (EConstr.of_constr body) in
   Sigma.Unsafe.of_pair ((body, expected_goal), sigma)
 
 (* Like "replace" but decompose dependent equalities                      *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2aa434777..63d10573a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -910,7 +910,7 @@ let make_mode ref m =
 let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
-  let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma c)) in
+  let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma (EConstr.of_constr c))) in
   let hd = head_of_constr_reference (head_constr sigma t) in
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 38f75995b..9282af759 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -123,13 +123,13 @@ let make_inv_predicate env evd indf realargs id status concl =
         let refl_term = eqdata.Coqlib.refl in
 	let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in
         let refl = mkApp (refl_term, [|eqnty; rhs|]) in
-	let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in
+	let _ = Evarutil.evd_comb1 (Typing.type_of env) evd (EConstr.of_constr refl) in
         let args = refl :: args in
         build_concl eqns args (succ n) restlist
   in
   let (newconcl, args) = build_concl [] [] 0 realargs in
   let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in
-  let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in
+  let _ = Evarutil.evd_comb1 (Typing.type_of env) evd (EConstr.of_constr predicate) in
   (* OK - this predicate should now be usable by res_elimination_then to
      do elimination on the conclusion. *)
   predicate, args
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c2163a274..8fb47b994 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -210,7 +210,7 @@ let convert_concl ?(check=true) ty k =
       let Sigma ((), sigma, p) =
         if check then begin
           let sigma = Sigma.to_evar_map sigma in
-          ignore (Typing.unsafe_type_of env sigma ty);
+          ignore (Typing.unsafe_type_of env sigma (EConstr.of_constr ty));
           let sigma,b = Reductionops.infer_conv env sigma ty conclty in
           if not b then error "Not convertible.";
           Sigma.Unsafe.of_pair ((), sigma)
@@ -827,7 +827,7 @@ let change_on_subterm cv_pb deep t where = { e_redfun = begin fun env sigma c ->
         env sigma c in
   if !mayneedglobalcheck then
     begin
-      try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map sigma) c)
+      try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map sigma) (EConstr.of_constr c))
       with e when catchable_exception e ->
         error "Replacement would lead to an ill-typed term."
     end;
@@ -1228,7 +1228,7 @@ let cut c =
     let is_sort =
       try
         (** Backward compat: ensure that [c] is well-typed. *)
-        let typ = Typing.unsafe_type_of env sigma c in
+        let typ = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in
         let typ = whd_all env sigma (EConstr.of_constr typ) in
         match kind_of_term typ with
         | Sort _ -> true
@@ -1940,7 +1940,7 @@ let exact_check c =
   let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   let env = Proofview.Goal.env gl in
   let sigma = Sigma.to_evar_map sigma in
-  let sigma, ct = Typing.type_of env sigma c in
+  let sigma, ct = Typing.type_of env sigma (EConstr.of_constr c) in
   let tac =
       Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c)
   in
@@ -2009,20 +2009,20 @@ exception DependsOnBody of Id.t option
 let check_is_type env sigma ty =
   let evdref = ref sigma in
   try
-    let _ = Typing.e_sort_of env evdref ty in
+    let _ = Typing.e_sort_of env evdref (EConstr.of_constr ty) in
     !evdref
   with e when CErrors.noncritical e ->
     raise (DependsOnBody None)
 
 let check_decl env sigma decl =
   let open Context.Named.Declaration in
-  let ty = NamedDecl.get_type decl in
+  let ty = EConstr.of_constr (NamedDecl.get_type decl) in
   let evdref = ref sigma in
   try
     let _ = Typing.e_sort_of env evdref ty in
     let _ = match decl with
     | LocalAssum _ -> ()
-    | LocalDef (_,c,_) -> Typing.e_check env evdref c ty
+    | LocalDef (_,c,_) -> Typing.e_check env evdref (EConstr.of_constr c) ty
     in
     !evdref
   with e when CErrors.noncritical e ->
@@ -2622,7 +2622,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
           let refl = applist (refl, [t;mkVar id]) in
 	  let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in
 	  let sigma = Sigma.to_evar_map sigma in
-	  let sigma, _ = Typing.type_of env sigma term in
+	  let sigma, _ = Typing.type_of env sigma (EConstr.of_constr term) in
           let ans = term,
             Tacticals.New.tclTHEN
 	      (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false)
@@ -2783,7 +2783,7 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
 let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
   let env = Tacmach.pf_env gl in
   let ids = Tacmach.pf_ids_of_hyps gl in
-  let sigma, t = Typing.type_of env sigma c in
+  let sigma, t = Typing.type_of env sigma (EConstr.of_constr c) in
   generalize_goal_gen env sigma ids i o t cl
 
 let old_generalize_dep ?(with_let=false) c gl =
@@ -2818,7 +2818,7 @@ let old_generalize_dep ?(with_let=false) c gl =
   let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
     (cl',project gl) in
   (** Check that the generalization is indeed well-typed *)
-  let (evd, _) = Typing.type_of env evd cl'' in
+  let (evd, _) = Typing.type_of env evd (EConstr.of_constr cl'') in
   let args = Context.Named.to_instance to_quantify_rev in
   tclTHENLIST
     [tclEVARS evd;
@@ -2836,7 +2836,7 @@ let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun
     List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr
       (Tacmach.New.pf_concl gl,Tacmach.New.project gl)
   in
-  let (evd, _) = Typing.type_of env evd newcl in
+  let (evd, _) = Typing.type_of env evd (EConstr.of_constr newcl) in
   let map ((_, c, b),_) = if Option.is_empty b then Some c else None in
   let tac = apply_type newcl (List.map_filter map lconstr) in
   Sigma.Unsafe.of_pair (tac, evd)
@@ -2853,7 +2853,7 @@ let new_generalize_gen_let lconstr =
     let newcl, sigma, args =
       List.fold_right_i 
 	(fun i ((_,c,b),_ as o) (cl, sigma, args) ->
-	  let sigma, t = Typing.type_of env sigma c in
+	  let sigma, t = Typing.type_of env sigma (EConstr.of_constr c) in
 	  let args = if Option.is_empty b then c :: args else args in
           let cl, sigma = generalize_goal_gen env sigma ids i o t cl in
           (cl, sigma, args))
@@ -4738,7 +4738,7 @@ let prove_transitivity hdcncl eq_kind t =
       let env = Proofview.Goal.env gl in
       let sigma = Tacmach.New.project gl in
       let type_of = Typing.unsafe_type_of env sigma in
-      let typt = type_of t in
+      let typt = type_of (EConstr.of_constr t) in
         (mkApp(hdcncl, [| typ1; c1; typt ;t |]),
          mkApp(hdcncl, [| typt; t; typ2; c2 |]))
   in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 5aa000b16..86fd4d9a2 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -206,7 +206,7 @@ let build_id_coercion idf_opt source poly =
   let _ =
     if not
       (Reductionops.is_conv_leq env sigma
-	(EConstr.of_constr (Typing.unsafe_type_of env sigma val_f)) (EConstr.of_constr typ_f))
+	(EConstr.of_constr (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f))) (EConstr.of_constr typ_f))
     then
       user_err  (strbrk
 	"Cannot be defined as coercion (maybe a bad number of arguments).")
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 14a45f837..c6dd3eb99 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -953,7 +953,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
   let rel, _ = interp_constr_evars_impls env evdref r in
-  let relty = Typing.unsafe_type_of env !evdref rel in
+  let relty = Typing.unsafe_type_of env !evdref (EConstr.of_constr rel) in
   let relargty =
     let error () =
       user_err ~loc:(constr_loc r)
@@ -1034,7 +1034,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
 	       ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
 	     prop |])
   in
-  let def = Typing.e_solve_evars env evdref def in
+  let def = Typing.e_solve_evars env evdref (EConstr.of_constr def) in
   let _ = evdref := Evarutil.nf_evar_map !evdref in
   let def = mkApp (def, [|intern_body_lam|]) in
   let binders_rel = nf_evar_context !evdref binders_rel in
@@ -1105,11 +1105,11 @@ let interp_recursive isfix fixl notations =
     List.fold_left2
       (fun env' id t ->
 	 if Flags.is_program_mode () then
-	   let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in
+	   let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref (EConstr.of_constr t) in
 	   let fixprot =
 	     try 
 	       let app = mkApp (delayed_force fix_proto, [|sort; t|]) in
-		 Typing.e_solve_evars env evdref app
+		 Typing.e_solve_evars env evdref (EConstr.of_constr app)
 	     with e  when CErrors.noncritical e -> t
 	   in
 	     LocalAssum (id,fixprot) :: env'