Namegen primitives now apply on evar constrs.

Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.

11 files changed, 143 insertions, 128 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a5a5fe6d2..490bc2801 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -708,7 +708,7 @@ let merge_name get_name obj = function
 
 let merge_names get_name = List.map2 (merge_name get_name)
 
-let get_names env sign eqns =
+let get_names env sigma sign eqns =
   let names1 = List.make (Context.Rel.length sign) Anonymous in
   (* If any, we prefer names used in pats, from top to bottom *)
   let names2,aliasname =
@@ -727,7 +727,7 @@ let get_names env sign eqns =
       (fun (l,avoid) d na ->
 	 let na =
 	   merge_name
-	     (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env (EConstr.Unsafe.to_constr t) na) avoid))
+	     (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid))
 	     d na
 	 in
          (na::l,(out_name na)::avoid))
@@ -924,7 +924,7 @@ let rec extract_predicate ccl = function
       ccl
 
 let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
-  let sign = make_arity_signature env true indf in
+  let sign = make_arity_signature env sigma true indf in
   (* n is the number of real args + 1 (+ possible let-ins in sign) *)
   let n = List.length sign in
   (* Before abstracting we generalize over cur and on those realargs *)
@@ -945,7 +945,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
   let pred = extract_predicate ccl tms in
   (* Build the predicate properly speaking *)
   let sign = List.map2 set_name (na::names) sign in
-  EConstr.of_constr (it_mkLambda_or_LetIn_name env (EConstr.Unsafe.to_constr pred) sign)
+  it_mkLambda_or_LetIn_name env sigma pred sign
 
 (* [expand_arg] is used by [specialize_predicate]
    if Yk denotes [Xk;xk] or [Xk],
@@ -1238,7 +1238,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   (* that had matched constructor C *)
   let cs_args = const_info.cs_args in
   let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs_args in
-  let names,aliasname = get_names pb.env cs_args eqns in
+  let names,aliasname = get_names pb.env !(pb.evdref) cs_args eqns in
   let typs = List.map2 RelDecl.set_name names cs_args
   in
 
@@ -1714,7 +1714,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
 
 let build_inversion_problem loc env sigma tms t =
   let make_patvar t (subst,avoid) =
-    let id = next_name_away (named_hd env (EConstr.Unsafe.to_constr t) Anonymous) avoid in
+    let id = next_name_away (named_hd env sigma t Anonymous) avoid in
     PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in
   let rec reveal_pattern t (subst,avoid as acc) =
     match EConstr.kind sigma (whd_all env sigma t) with
@@ -1733,8 +1733,7 @@ let build_inversion_problem loc env sigma tms t =
 	let patl,acc = List.fold_map' reveal_pattern realargs acc in
 	let pat,acc = make_patvar t acc in
 	let indf' = lift_inductive_family n indf in
-	let sign = make_arity_signature env true indf' in
-	let sign = List.map (fun d -> map_rel_decl EConstr.of_constr d) sign in
+	let sign = make_arity_signature env sigma true indf' in
         let patl = pat :: List.rev patl in
 	let patl,sign = recover_and_adjust_alias_names patl sign in
 	let p = List.length patl in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c8d945c0b..1adda14ab 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,14 +6,17 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module CVars = Vars
+
 open Pp
 open CErrors
 open Util
 open Names
 open Term
+open Environ
+open EConstr
 open Vars
 open Inductiveops
-open Environ
 open Glob_term
 open Glob_ops
 open Termops
@@ -188,7 +191,7 @@ let _ = declare_bool_option
 (* Auxiliary function for MutCase printing *)
 (* [computable] tries to tell if the predicate typing the result is inferable*)
 
-let computable p k =
+let computable sigma p k =
     (* We first remove as many lambda as the arity, then we look
        if it remains a lambda for a dependent elimination. This function
        works for normal eta-expanded term. For non eta-expanded or
@@ -205,31 +208,29 @@ let computable p k =
        sinon on perd la réciprocité de la synthèse (qui, lui,
        engendrera un prédicat non dépendant) *)
 
-  let sign,ccl = decompose_lam_assum p in
+  let sign,ccl = decompose_lam_assum sigma p in
   Int.equal (Context.Rel.length sign) (k + 1)
   &&
-  noccur_between 1 (k+1) ccl
+  noccur_between sigma 1 (k+1) ccl
 
-let pop t = Vars.lift (-1) t
-
-let lookup_name_as_displayed env t s =
-  let rec lookup avoid n c = match kind_of_term c with
+let lookup_name_as_displayed env sigma t s =
+  let rec lookup avoid n c = match EConstr.kind sigma c with
     | Prod (name,_,c') ->
-	(match compute_displayed_name_in RenamingForGoal avoid name c' with
+	(match compute_displayed_name_in sigma RenamingForGoal avoid name c' with
            | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
 	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
     | LetIn (name,_,_,c') ->
-	(match compute_displayed_name_in RenamingForGoal avoid name c' with
+	(match compute_displayed_name_in sigma RenamingForGoal avoid name c' with
            | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
 	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
     | Cast (c,_,_) -> lookup avoid n c
     | _ -> None
   in lookup (ids_of_named_context (named_context env)) 1 t
 
-let lookup_index_as_renamed env t n =
-  let rec lookup n d c = match kind_of_term c with
+let lookup_index_as_renamed env sigma t n =
+  let rec lookup n d c = match EConstr.kind sigma c with
     | Prod (name,_,c') ->
-	  (match compute_displayed_name_in RenamingForGoal [] name c' with
+	  (match compute_displayed_name_in sigma RenamingForGoal [] name c' with
                (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) ->
 		 if Int.equal n 0 then
@@ -239,7 +240,7 @@ let lookup_index_as_renamed env t n =
 		 else
 		   lookup (n-1) (d+1) c')
     | LetIn (name,_,_,c') ->
-	  (match compute_displayed_name_in RenamingForGoal [] name c' with
+	  (match compute_displayed_name_in sigma RenamingForGoal [] name c' with
              | (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) ->
 		 if Int.equal n 0 then
@@ -256,9 +257,9 @@ let lookup_index_as_renamed env t n =
 (**********************************************************************)
 (* Fragile algorithm to reverse pattern-matching compilation          *)
 
-let update_name na ((_,(e,_)),c) =
+let update_name sigma na ((_,(e,_)),c) =
   match na with
-  | Name _ when force_wildcard () && noccurn (List.index Name.equal na e) c ->
+  | Name _ when force_wildcard () && noccurn sigma (List.index Name.equal na e) c ->
       Anonymous
   | _ ->
       na
@@ -269,7 +270,7 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c =
   | [] -> (List.rev nal,(e,c))
   | b::tags ->
       let na,c,f,body,t =
-        match kind_of_term (EConstr.Unsafe.to_constr (strip_outer_cast sigma (EConstr.of_constr c))), b with
+        match EConstr.kind sigma (strip_outer_cast sigma c), b with
 	| Lambda (na,t,c),false -> na,c,compute_displayed_let_name_in,None,Some t
 	| LetIn (na,b,t,c),true ->
             na,c,compute_displayed_name_in,Some b,Some t
@@ -279,12 +280,12 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c =
 	| _, true ->
 	  Anonymous,lift 1 c,compute_displayed_name_in,None,None
     in
-    let na',avoid' = f flag avoid na c in
+    let na',avoid' = f sigma flag avoid na c in
     decomp_branch tags (na'::nal) b
       (avoid', add_name_opt na' body t env) sigma c
 
 let rec build_tree na isgoal e sigma ci cl =
-  let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
+  let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name sigma na rhs) in
   let cnl = ci.ci_pp_info.cstr_tags in
   let cna = ci.ci_cstr_nargs in
   List.flatten
@@ -294,12 +295,12 @@ let rec build_tree na isgoal e sigma ci cl =
 and align_tree nal isgoal (e,c as rhs) sigma = match nal with
   | [] -> [[],rhs]
   | na::nal ->
-    match kind_of_term c with
+    match EConstr.kind sigma c with
     | Case (ci,p,c,cl) when
-        eq_constr sigma (EConstr.of_constr c) (EConstr.mkRel (List.index Name.equal na (fst (snd e))))
+        eq_constr sigma c (mkRel (List.index Name.equal na (fst (snd e))))
         && not (Int.equal (Array.length cl) 0)
 	&& (* don't contract if p dependent *)
-	computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
+	computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
 	let clauses = build_tree na isgoal e sigma ci cl in
 	List.flatten
           (List.map (fun (pat,rhs) ->
@@ -307,7 +308,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
 	      List.map (fun (hd,rest) -> pat::hd,rest) lines)
 	    clauses)
     | _ ->
-	let pat = PatVar(dl,update_name na rhs) in
+	let pat = PatVar(dl,update_name sigma na rhs) in
 	let mat = align_tree nal isgoal rhs sigma in
 	List.map (fun (hd,rest) -> pat::hd,rest) mat
 
@@ -320,11 +321,11 @@ and contract_branch isgoal e sigma (cdn,can,mkpat,b) =
 (* Transform internal representation of pattern-matching into list of *)
 (* clauses                                                            *)
 
-let is_nondep_branch c l =
+let is_nondep_branch sigma c l =
   try
     (* FIXME: do better using tags from l *)
-    let sign,ccl = decompose_lam_n_decls (List.length l) c in
-    noccur_between 1 (Context.Rel.length sign) ccl
+    let sign,ccl = decompose_lam_n_decls sigma (List.length l) c in
+    noccur_between sigma 1 (Context.Rel.length sign) ccl
   with e when CErrors.noncritical e -> (* Not eta-expanded or not reduced *)
     false
 
@@ -441,7 +442,7 @@ let detype_instance sigma l =
   else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
 
 let rec detype flags avoid env sigma t =
-  match kind_of_term (EConstr.Unsafe.to_constr (collapse_appl sigma (EConstr.of_constr t))) with
+  match EConstr.kind sigma (collapse_appl sigma t) with
     | Rel n ->
       (try match lookup_name_of_rel n (fst env) with
 	 | Name id   -> GVar (dl, id)
@@ -503,11 +504,11 @@ let rec detype flags avoid env sigma t =
 	    try 
 	      let pb = Environ.lookup_projection p (snd env) in
 	      let body = pb.Declarations.proj_body in
-	      let ty = Retyping.get_type_of (snd env) sigma (EConstr.of_constr c) in
+	      let ty = Retyping.get_type_of (snd env) sigma c in
 	      let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
-	      let args = List.map EConstr.Unsafe.to_constr args in
 	      let body' = strip_lam_assum body in
-	      let body' = subst_instance_constr u body' in
+	      let body' = CVars.subst_instance_constr u body' in
+	      let body' = EConstr.of_constr body' in
 		substl (c :: List.rev args) body'
 	    with Retyping.RetypeError _ | Not_found -> 
 	      anomaly (str"Cannot detype an unfolded primitive projection.")
@@ -515,8 +516,7 @@ let rec detype flags avoid env sigma t =
 	else
 	  if print_primproj_params () then
 	    try
-	      let c = Retyping.expand_projection (snd env) sigma p (EConstr.of_constr c) [] in
-	      let c = EConstr.Unsafe.to_constr c in
+	      let c = Retyping.expand_projection (snd env) sigma p c [] in
 		detype flags avoid env sigma c
 	    with Retyping.RetypeError _ -> noparams ()
 	  else noparams ()
@@ -527,8 +527,8 @@ let rec detype flags avoid env sigma t =
           | LocalDef _ -> true
           | LocalAssum (id,_) ->
 	     try let n = List.index Name.equal (Name id) (fst env) in
-	         isRelN n c
-	     with Not_found -> isVarId id c
+	         isRelN sigma n c
+	     with Not_found -> isVarId sigma id c
         in
       let id,l =
         try
@@ -537,8 +537,8 @@ let rec detype flags avoid env sigma t =
           | Some id -> id
           in
           let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
-          let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
-          let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
+          let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match EConstr.kind sigma c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
+          let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in
           id,l
         with Not_found ->
           Id.of_string ("X" ^ string_of_int (Evar.repr evk)), 
@@ -551,10 +551,10 @@ let rec detype flags avoid env sigma t =
     | Construct (cstr_sp,u) ->
 	GRef (dl, ConstructRef cstr_sp, detype_instance sigma u)
     | Case (ci,p,c,bl) ->
-	let comp = computable p (List.length (ci.ci_pp_info.ind_tags)) in
+	let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in
 	detype_case comp (detype flags avoid env sigma)
 	  (detype_eqns flags avoid env sigma ci comp)
-	  is_nondep_branch avoid
+	  (is_nondep_branch sigma) avoid
 	  (ci.ci_ind,ci.ci_pp_info.style,
 	   ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
 	  (Some p) c bl
@@ -594,7 +594,7 @@ and detype_cofix flags avoid env sigma n (names,tys,bodies) =
        Array.map (fun (_,bd,_) -> bd) v)
 
 and share_names flags n l avoid env sigma c t =
-  match kind_of_term c, kind_of_term t with
+  match EConstr.kind sigma c, EConstr.kind sigma t with
     (* factorize even when not necessary to have better presentation *)
     | Lambda (na,t,c), Prod (na',t',c') ->
         let na = match (na,na') with
@@ -641,15 +641,15 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
 
 and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch =
   let make_pat x avoid env b body ty ids =
-    if force_wildcard () && noccurn 1 b then
+    if force_wildcard () && noccurn sigma 1 b then
       PatVar (dl,Anonymous),avoid,(add_name Anonymous body ty env),ids
     else
       let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in
-      let na,avoid' = compute_displayed_name_in flag avoid x b in
+      let na,avoid' = compute_displayed_name_in sigma flag avoid x b in
       PatVar (dl,na),avoid',(add_name na body ty env),add_vname ids na
   in
   let rec buildrec ids patlist avoid env l b =
-    match kind_of_term b, l with
+    match EConstr.kind sigma b, l with
       | _, [] ->
         (dl, Id.Set.elements ids,
          [PatCstr(dl, constr, List.rev patlist,Anonymous)],
@@ -684,8 +684,8 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
 and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
   let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in
   let na',avoid' = match bk with
-  | BLetIn -> compute_displayed_let_name_in flag avoid na c
-  | _ -> compute_displayed_name_in flag avoid na c in
+  | BLetIn -> compute_displayed_let_name_in sigma flag avoid na c
+  | _ -> compute_displayed_name_in sigma flag avoid na c in
   let r =  detype flags avoid' (add_name na' body ty env) sigma c in
   match bk with
   | BProd -> GProd (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r)
@@ -693,13 +693,13 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
   | BLetIn ->
       let c = detype (lax,false) avoid env sigma (Option.get body) in
       (* Heuristic: we display the type if in Prop *)
-      let s = try Retyping.get_sort_family_of (snd env) sigma (EConstr.of_constr ty) with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
+      let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
       let c = if s != InProp then c else
           GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in
       GLetIn (dl, na', c, r)
 
 let detype_rel_context ?(lax=false) where avoid env sigma sign =
-  let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
+  let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in
   let rec aux avoid env = function
   | [] -> []
   | decl::rest ->
@@ -711,10 +711,10 @@ let detype_rel_context ?(lax=false) where avoid env sigma sign =
 	| None -> na,avoid
 	| Some c ->
 	    if is_local_def decl then
-	      compute_displayed_let_name_in
+	      compute_displayed_let_name_in sigma
                 (RenamingElsewhereFor (fst env,c)) avoid na c
 	    else
-	      compute_displayed_name_in
+	      compute_displayed_name_in sigma
                 (RenamingElsewhereFor (fst env,c)) avoid na c in
       let b = match decl with
 	      | LocalAssum _ -> None
@@ -731,6 +731,7 @@ let detype ?(lax=false) isgoal avoid env sigma t =
   detype (lax,isgoal) avoid (names_of_rel_context env, env) sigma t
 
 let detype_closed_glob ?lax isgoal avoid env sigma t =
+  let open Context.Rel.Declaration in
   let convert_id cl id =
     try Id.Map.find id cl.idents
     with Not_found -> id
@@ -748,12 +749,11 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
         with Not_found -> try
           (* assumes [detype] does not raise [Not_found] exceptions *)
           let (b,c) = Id.Map.find id cl.typed in
-          let c = EConstr.Unsafe.to_constr c in
           (* spiwack: I'm not sure it is the right thing to do,
              but I'm computing the detyping environment like
              [Printer.pr_constr_under_binders_env] does. *)
-          let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) b in
-          let env = Termops.push_rels_assum assums env in
+          let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in
+          let env = push_rel_context assums env in
           detype ?lax isgoal avoid env sigma c
         (* if [id] is bound to a [closed_glob_constr]. *)
         with Not_found -> try
@@ -808,7 +808,7 @@ let rec subst_glob_constr subst raw =
   | GRef (loc,ref,u) ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then raw else
-         detype false [] (Global.env()) Evd.empty t
+         detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)
 
   | GVar _ -> raw
   | GEvar _ -> raw
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index c51cb0f44..4c6f9129f 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -9,6 +9,7 @@
 open Names
 open Term
 open Environ
+open EConstr
 open Glob_term
 open Termops
 open Mod_subst
@@ -45,13 +46,13 @@ val detype_case :
 val detype_sort : evar_map -> sorts -> glob_sort
 
 val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> 
-  evar_map -> Context.Rel.t -> glob_decl list
+  evar_map -> rel_context -> glob_decl list
 
 val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr
 
 (** look for the index of a named var or a nondep var as it is renamed *)
-val lookup_name_as_displayed  : env -> constr -> Id.t -> int option
-val lookup_index_as_renamed : env -> constr -> int -> int option
+val lookup_name_as_displayed  : env -> evar_map -> constr -> Id.t -> int option
+val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option
 
 val set_detype_anonymous : (Loc.t -> int -> glob_constr) -> unit
 val force_wildcard : unit -> bool
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index faf34baf7..20d86f81b 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -140,7 +140,7 @@ let define_pure_evar_as_lambda env evd evk =
   | _ -> error_not_product env evd typ in
   let avoid = ids_of_named_context (evar_context evi) in
   let id =
-    next_name_away_with_default_using_types "x" na avoid (EConstr.Unsafe.to_constr (Reductionops.whd_evar evd dom)) in
+    next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in
   let newenv = push_named (LocalAssum (id, dom)) evenv in
   let filter = Filter.extend 1 (evar_filter evi) in
   let src = evar_source evk evd1 in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 431d1ff16..c4a74d990 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -40,6 +40,18 @@ type recursion_scheme_error =
 
 exception RecursionSchemeError of recursion_scheme_error
 
+let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na
+let name_assumption env = function
+| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
+| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
+
+let mkLambda_or_LetIn_name env d b = mkLambda_or_LetIn (name_assumption env d) b
+let mkProd_or_LetIn_name env d b = mkProd_or_LetIn (name_assumption env d) b
+let mkLambda_name env (n,a,b) = mkLambda_or_LetIn_name env (LocalAssum (n,a)) b
+let mkProd_name env (n,a,b) = mkProd_or_LetIn_name env (LocalAssum (n,a)) b
+let it_mkProd_or_LetIn_name env b l = List.fold_left (fun c d -> mkProd_or_LetIn_name env d c) b l
+let it_mkLambda_or_LetIn_name env b l = List.fold_left (fun c d -> mkLambda_or_LetIn_name env d c) b l
+
 let make_prod_dep dep env = if dep then mkProd_name env else mkProd
 let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c)
 
@@ -118,12 +130,13 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
 	it_mkLambda_or_LetIn_name env' obj deparsign
     else
       let cs = lift_constructor (k+1) constrs.(k) in
-      let t = build_branch_type env dep (mkRel (k+1)) cs in
+      let t = build_branch_type env (Sigma.to_evar_map sigma) dep (mkRel (k+1)) cs in
       mkLambda_string "f" t
 	(add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1))
   in
   let Sigma (s, sigma, p) = Sigma.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in
-  let typP = make_arity env' dep indf s in
+  let typP = make_arity env' (Sigma.to_evar_map sigma) dep indf s in
+  let typP = EConstr.Unsafe.to_constr typP in
   let c = 
     it_mkLambda_or_LetIn_name env
     (mkLambda_string "P" typP
@@ -443,7 +456,8 @@ let mis_make_indrec env sigma listdepkind mib u =
 	    Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env) 
 	      evdref kinds 
 	  in
-	  let typP = make_arity env dep indf s in
+	  let typP = make_arity env !evdref dep indf s in
+	  let typP = EConstr.Unsafe.to_constr typP in
 	    mkLambda_string "P" typP
 	      (put_arity (push_rel (LocalAssum (Anonymous,typP)) env) (i+1) rest)
       | [] ->
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 3191a58ff..9e823ab4c 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -422,26 +422,29 @@ let build_dependent_inductive env ((ind, params) as indf) =
 
 (* builds the arity of an elimination predicate in sort [s] *)
 
-let make_arity_signature env dep indf =
+let make_arity_signature env sigma dep indf =
   let (arsign,_) = get_arity env indf in
+  let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in
   if dep then
     (* We need names everywhere *)
-    Namegen.name_context env
-      ((LocalAssum (Anonymous,build_dependent_inductive env indf))::arsign)
+    Namegen.name_context env sigma
+      ((LocalAssum (Anonymous,EConstr.of_constr (build_dependent_inductive env indf)))::arsign)
       (* Costly: would be better to name once for all at definition time *)
   else
     (* No need to enforce names *)
     arsign
 
-let make_arity env dep indf s = mkArity (make_arity_signature env dep indf, s)
+let make_arity env sigma dep indf s =
+  let open EConstr in
+  it_mkProd_or_LetIn (mkSort s) (make_arity_signature env sigma dep indf)
 
 (* [p] is the predicate and [cs] a constructor summary *)
-let build_branch_type env dep p cs =
+let build_branch_type env sigma dep p cs =
   let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in
   if dep then
-    Namegen.it_mkProd_or_LetIn_name env
-      (applist (base,[build_dependent_constructor cs]))
-      cs.cs_args
+    EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma
+      (EConstr.of_constr (applist (base,[build_dependent_constructor cs])))
+      (List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) cs.cs_args))
   else
     Term.it_mkProd_or_LetIn base cs.cs_args
 
@@ -542,11 +545,12 @@ let is_elim_predicate_explicitly_dependent env sigma pred indf =
   let arsign,_ = get_arity env indf in
   is_predicate_explicitly_dep env sigma pred arsign
 
-let set_names env n brty =
-  let (ctxt,cl) = decompose_prod_n_assum n brty in
-  Namegen.it_mkProd_or_LetIn_name env cl ctxt
+let set_names env sigma n brty =
+  let open EConstr in
+  let (ctxt,cl) = decompose_prod_n_assum sigma n brty in
+  EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt)
 
-let set_pattern_names env ind brv =
+let set_pattern_names env sigma ind brv =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let arities =
     Array.map
@@ -554,7 +558,7 @@ let set_pattern_names env ind brv =
         Context.Rel.length ((prod_assum c)) -
         mib.mind_nparams)
       mip.mind_nf_lc in
-  Array.map2 (set_names env) arities brv
+  Array.map2 (set_names env sigma) arities brv
 
 let type_case_branches_with_names env sigma indspec p c =
   let (ind,args) = indspec in
@@ -567,7 +571,7 @@ let type_case_branches_with_names env sigma indspec p c =
   let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
   (* Adjust names *)
   if is_elim_predicate_explicitly_dependent env sigma p (ind,params) then
-    (set_pattern_names env (fst ind) lbrty, conclty)
+    (set_pattern_names env sigma (fst ind) (Array.map EConstr.of_constr lbrty), conclty)
   else (lbrty, conclty)
 
 (* Type of Case predicates *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 4bb484759..ab470a540 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -156,9 +156,9 @@ val get_arity        : env -> inductive_family -> Context.Rel.t * sorts_family
 
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive_family -> constr
-val make_arity_signature : env -> bool -> inductive_family -> Context.Rel.t
-val make_arity : env -> bool -> inductive_family -> sorts -> types
-val build_branch_type : env -> bool -> constr -> constructor_summary -> types
+val make_arity_signature : env -> evar_map -> bool -> inductive_family -> EConstr.rel_context
+val make_arity : env -> evar_map -> bool -> inductive_family -> sorts -> EConstr.types
+val build_branch_type : env -> evar_map -> bool -> constr -> constructor_summary -> types
 
 (** Raise [Not_found] if not given a valid inductive type *)
 val extract_mrectype : evar_map -> EConstr.t -> pinductive * EConstr.constr list
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2470decdd..563769df5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -79,26 +79,26 @@ type t = {
   (** Delay the computation of the evar extended environment *)
 }
 
-let get_extra env =
+let get_extra env sigma =
   let open Context.Named.Declaration in
   let ids = List.map get_id (named_context env) in
   let avoid = List.fold_right Id.Set.add ids Id.Set.empty in
-  Context.Rel.fold_outside push_rel_decl_to_named_context
+  Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
     (rel_context env) ~init:(empty_csubst, [], avoid, named_context env)
 
-let make_env env = { env = env; extra = lazy (get_extra env) }
+let make_env env sigma = { env = env; extra = lazy (get_extra env sigma) }
 let rel_context env = rel_context env.env
 
-let push_rel d env = {
+let push_rel sigma d env = {
   env = push_rel d env.env;
-  extra = lazy (push_rel_decl_to_named_context d (Lazy.force env.extra));
+  extra = lazy (push_rel_decl_to_named_context sigma d (Lazy.force env.extra));
 }
 
-let pop_rel_context n env = make_env (pop_rel_context n env.env)
+let pop_rel_context n env sigma = make_env (pop_rel_context n env.env) sigma
 
-let push_rel_context ctx env = {
+let push_rel_context sigma ctx env = {
   env = push_rel_context ctx env.env;
-  extra = lazy (List.fold_right push_rel_decl_to_named_context ctx (Lazy.force env.extra));
+  extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx (Lazy.force env.extra));
 }
 
 let lookup_named id env = lookup_named id env.env
@@ -117,9 +117,9 @@ let e_new_evar env evdref ?src ?naming typ =
   evdref := Sigma.to_evar_map sigma;
   e
 
-let push_rec_types (lna,typarray,_) env =
+let push_rec_types sigma (lna,typarray,_) env =
   let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in
-  Array.fold_left (fun e assum -> push_rel assum e) env ctxt
+  Array.fold_left (fun e assum -> push_rel sigma assum e) env ctxt
 
 end
 
@@ -391,7 +391,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function
                            str"It cannot be used in a binder.")
         else n
 
-let ltac_interp_name_env k0 lvar env =
+let ltac_interp_name_env k0 lvar env sigma =
   (* envhd is the initial part of the env when pretype was called first *)
   (* (in practice is is probably 0, but we have to grant the
      specification of pretype which accepts to start with a non empty
@@ -402,7 +402,7 @@ let ltac_interp_name_env k0 lvar env =
   let open Context.Rel.Declaration in
   let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in
   if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env
-  else push_rel_context ctxt' (pop_rel_context n env)
+  else push_rel_context sigma ctxt' (pop_rel_context n env sigma)
 
 let invert_ltac_bound_name lvar env id0 id =
   let id' = Id.Map.find id lvar.ltac_idents in
@@ -426,7 +426,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
     let (n,_,typ) = lookup_rel_id id (rel_context env) in
       { uj_val  = mkRel n; uj_type = lift n typ }
   with Not_found ->
-    let env = ltac_interp_name_env k0 lvar env in
+    let env = ltac_interp_name_env k0 lvar env !evdref in
     (* Check if [id] is an ltac variable *)
     try
       let (ids,c) = Id.Map.find id lvar.ltac_constrs in
@@ -569,7 +569,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	inh_conv_coerce_to_tycon loc env evdref j tycon
 
   | GPatVar (loc,(someta,n)) ->
-    let env = ltac_interp_name_env k0 lvar env in
+    let env = ltac_interp_name_env k0 lvar env !evdref in
     let ty =
       match tycon with
       | Some ty -> ty
@@ -578,7 +578,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
 
   | GHole (loc, k, naming, None) ->
-      let env = ltac_interp_name_env k0 lvar env in
+      let env = ltac_interp_name_env k0 lvar env !evdref in
       let ty =
         match tycon with
         | Some ty -> ty
@@ -587,7 +587,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty }
 
   | GHole (loc, k, _naming, Some arg) ->
-      let env = ltac_interp_name_env k0 lvar env in
+      let env = ltac_interp_name_env k0 lvar env !evdref in
       let ty =
         match tycon with
         | Some ty -> ty
@@ -605,18 +605,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         let ty' = pretype_type empty_valcon env evdref lvar ty in
 	let dcl = LocalAssum (na, ty'.utj_val) in
         let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in
-	  type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl
+	  type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl
       | (na,bk,Some bd,ty)::bl ->
         let ty' = pretype_type empty_valcon env evdref lvar ty in
         let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
         let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in
         let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in
-	  type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in
+	  type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl in
     let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in
     let larj =
       Array.map2
         (fun e ar ->
-          pretype_type empty_valcon (push_rel_context e env) evdref lvar ar)
+          pretype_type empty_valcon (push_rel_context !evdref e env) evdref lvar ar)
         ctxtv lar in
     let lara = Array.map (fun a -> a.utj_val) larj in
     let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
@@ -632,7 +632,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       | None -> true
     in
       (* Note: bodies are not used by push_rec_types, so [||] is safe *)
-    let newenv = push_rec_types (names,ftys,[||]) env in
+    let newenv = push_rec_types !evdref (names,ftys,[||]) env in
     let vdefj =
       Array.map2_i
 	(fun i ctxt def ->
@@ -641,7 +641,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
           let (ctxt,ty) =
 	    decompose_prod_n_assum !evdref (Context.Rel.length ctxt)
               (lift nbfix ftys.(i)) in
-          let nenv = push_rel_context ctxt newenv in
+          let nenv = push_rel_context !evdref ctxt newenv in
           let j = pretype (mk_tycon ty) nenv evdref lvar def in
 	    { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
 	      uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
@@ -783,7 +783,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
     let var = LocalAssum (name, j.utj_val) in
-    let j' = pretype rng (push_rel var env) evdref lvar c2 in
+    let j' = pretype rng (push_rel !evdref var env) evdref lvar c2 in
     let name = ltac_interp_name lvar name in
     let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
@@ -799,7 +799,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
           { j with utj_val = lift 1 j.utj_val }
       | Name _ ->
         let var = LocalAssum (name, j.utj_val) in
-        let env' = push_rel var env in
+        let env' = push_rel !evdref var env in
           pretype_type empty_valcon env' evdref lvar c2
     in
     let name = ltac_interp_name lvar name in
@@ -828,7 +828,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
        looked up in the rel context. *)
     let var = LocalDef (name, j.uj_val, t) in
     let tycon = lift_tycon 1 tycon in
-    let j' = pretype tycon (push_rel var env) evdref lvar c2 in
+    let j' = pretype tycon (push_rel !evdref var env) evdref lvar c2 in
     let name = ltac_interp_name lvar name in
       { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	uj_type = subst1 j.uj_val j'.uj_type }
@@ -877,7 +877,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  mkCase (ci, p, cj.uj_val,[|f|]) 
       else it_mkLambda_or_LetIn f fsign
     in
-    let env_f = push_rel_context fsign env in
+    let env_f = push_rel_context !evdref fsign env in
       (* Make dependencies from arity signature impossible *)
     let arsgn =
       let arsgn,_ = get_arity env.ExtraEnv.env indf in
@@ -890,11 +890,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       let nar = List.length arsgn in
 	  (match po with
 	  | Some p ->
-	    let env_p = push_rel_context psign env in
+	    let env_p = push_rel_context !evdref psign env in
 	    let pj = pretype_type empty_valcon env_p evdref lvar p in
 	    let ccl = nf_evar !evdref pj.utj_val in
-	    let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *)
-            let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
+	    let psign = make_arity_signature env.ExtraEnv.env !evdref true indf in (* with names *)
 	    let p = it_mkLambda_or_LetIn ccl psign in
 	    let inst =
 	      (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs)
@@ -951,7 +950,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
       let pred,p = match po with
 	| Some p ->
-	  let env_p = push_rel_context psign env in
+	  let env_p = push_rel_context !evdref psign env in
 	  let pj = pretype_type empty_valcon env_p evdref lvar p in
 	  let ccl = nf_evar !evdref pj.utj_val in
 	  let pred = it_mkLambda_or_LetIn ccl psign in
@@ -961,7 +960,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  let p = match tycon with
 	    | Some ty -> ty
 	    | None ->
-              let env = ltac_interp_name_env k0 lvar env in
+              let env = ltac_interp_name_env k0 lvar env !evdref in
               new_type_evar env evdref loc
 	  in
 	    it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
@@ -980,7 +979,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 				       | Anonymous -> Name Namegen.default_non_dependent_ident))
 		     cs_args
 	in
-	let env_c = push_rel_context csgn env in
+	let env_c = push_rel_context !evdref csgn env in
 	let bj = pretype (mk_tycon pi) env_c evdref lvar b in
 	  it_mkLambda_or_LetIn bj.uj_val cs_args in
       let b1 = f cstrs.(0) b1 in
@@ -997,7 +996,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 
   | GCases (loc,sty,po,tml,eqns) ->
     Cases.compile_cases loc sty
-      ((fun vtyc env evdref -> pretype vtyc (make_env env) evdref lvar),evdref)
+      ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref lvar),evdref)
       tycon env.ExtraEnv.env (* loc *) (po,tml,eqns)
 
   | GCast (loc,c,k) ->
@@ -1090,7 +1089,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
 	     { utj_val = v;
 	       utj_type = s }
        | None ->
-           let env = ltac_interp_name_env k0 lvar env in
+           let env = ltac_interp_name_env k0 lvar env !evdref in
 	   let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
 	     { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s);
 	       utj_type = s})
@@ -1107,7 +1106,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
                 ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
 
 let ise_pretype_gen flags env sigma lvar kind c =
-  let env = make_env env in
+  let env = make_env env sigma in
   let evdref = ref sigma in
   let k0 = Context.Rel.length (rel_context env) in
   let c' = match kind with
@@ -1150,7 +1149,7 @@ let on_judgment sigma f j =
   {uj_val = c; uj_type = t}
 
 let understand_judgment env sigma c =
-  let env = make_env env in
+  let env = make_env env sigma in
   let evdref = ref sigma in
   let k0 = Context.Rel.length (rel_context env) in
   let j = pretype k0 true empty_tycon env evdref empty_lvar c in
@@ -1160,7 +1159,7 @@ let understand_judgment env sigma c =
   in j, Evd.evar_universe_context !evdref
 
 let understand_judgment_tcc env evdref c =
-  let env = make_env env in
+  let env = make_env env !evdref in
   let k0 = Context.Rel.length (rel_context env) in
   let j = pretype k0 true empty_tycon env evdref empty_lvar c in
   on_judgment !evdref (fun c ->
@@ -1217,7 +1216,7 @@ let type_uconstr ?(flags = constr_flags)
   end }
 
 let pretype k0 resolve_tc typcon env evdref lvar t =
-  pretype k0 resolve_tc typcon (make_env env) evdref lvar t
+  pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t
 
 let pretype_type k0 resolve_tc valcon env evdref lvar t =
-  pretype_type k0 resolve_tc valcon (make_env env) evdref lvar t
+  pretype_type k0 resolve_tc valcon (make_env env !evdref) evdref lvar t
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9f3f3c7e5..ef9f39d77 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1141,7 +1141,7 @@ let compute = cbv_betadeltaiota
 
 let abstract_scheme env sigma (locc,a) (c, sigma) =
   let ta = Retyping.get_type_of env sigma a in
-  let na = named_hd env (EConstr.to_constr sigma ta) Anonymous in
+  let na = named_hd env sigma ta Anonymous in
   if occur_meta sigma ta then error "Cannot find a type for the generalisation.";
   if occur_meta sigma a then
     mkLambda (na,ta,c), sigma
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index bdd3663d1..dec22ecd0 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -92,8 +92,7 @@ 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 arsign = make_arity_signature env true (make_ind_family (ind,params)) in
-  let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in
+  let arsign = make_arity_signature env !evdref true (make_ind_family (ind,params)) in
   let allowed_sorts = elim_sorts specif in
   let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
   let rec srec env pt ar =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 589201fe2..baa12db08 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -85,7 +85,7 @@ let occur_meta_evd sigma mv c =
 
 let abstract_scheme env evd c l lname_typ =
   let mkLambda_name env (n,a,b) =
-    mkLambda (named_hd env (EConstr.Unsafe.to_constr a) n, a, b)
+    mkLambda (named_hd env evd a n, a, b)
   in
   List.fold_left2
     (fun (t,evd) (locc,a) decl ->
@@ -1617,8 +1617,7 @@ let make_eq_test env evd c =
 let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
   let id =
     let t = match ty with Some t -> t | None -> get_type_of env sigma c in
-    let t = EConstr.Unsafe.to_constr t in
-    let x = id_of_name_using_hdchar (Global.env()) t name in
+    let x = id_of_name_using_hdchar (Global.env()) sigma t name in
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context_val x (named_context_val env) then