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.

43 files changed, 351 insertions, 317 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 657285de2..7d4d17c63 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -131,6 +131,8 @@ let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false
 let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false
 let isVarId sigma id c =
   match kind sigma c with Var id' -> Id.equal id id' | _ -> false
+let isRelN sigma n c =
+  match kind sigma c with Rel n' -> Int.equal n n' | _ -> false
 
 let destRel sigma c = match kind sigma c with
 | Rel p -> p
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index d6b2113d2..83536d6f8 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -114,6 +114,7 @@ val isCase : Evd.evar_map -> t -> bool
 val isProj : Evd.evar_map -> t -> bool
 val isArity : Evd.evar_map -> t -> bool
 val isVarId  : Evd.evar_map -> Id.t -> t -> bool
+val isRelN : Evd.evar_map -> int -> t -> bool
 
 val destRel : Evd.evar_map -> t -> int
 val destMeta : Evd.evar_map -> t -> metavariable
diff --git a/engine/engine.mllib b/engine/engine.mllib
index c78f37a85..1b670d366 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,10 +1,10 @@
 Logic_monad
-Namegen
 Universes
 UState
 Evd
 Sigma
 EConstr
+Namegen
 Termops
 Proofview_monad
 Evarutil
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index e94fd72f1..ce6d06f23 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -326,7 +326,7 @@ let push_var id (n, s) =
   let s = Int.Map.add n (EConstr.mkVar id) s in
   (succ n, s)
 
-let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
+let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) =
   let open EConstr in
   let open Vars in
   let map_decl f d =
@@ -354,7 +354,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
     else
       (** id_of_name_using_hdchar only depends on the rel context which is empty
           here *)
-      next_ident_away (id_of_name_using_hdchar empty_env (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) na) avoid
+      next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid
   in
   match extract_if_neq id na with
   | Some id0 when not (is_section_variable id0) ->
@@ -375,7 +375,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
       let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (subst2 subst vsubst) in
       (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc)
 
-let push_rel_context_to_named_context env typ =
+let push_rel_context_to_named_context env sigma typ =
   (* compute the instances relative to the named context and rel_context *)
   let open Context.Named.Declaration in
   let open EConstr in
@@ -390,7 +390,7 @@ let push_rel_context_to_named_context env typ =
     (* with vars of the rel context *)
     (* We do keep the instances corresponding to local definition (see above) *)
     let (subst, vsubst, _, env) =
-      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) in
     (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
 
@@ -452,7 +452,7 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
 let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
-  let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
+  let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env (Sigma.to_evar_map evd) typ in
   let map c = subst2 subst vsubst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
   let instance =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 2da4f8043..da49d4e11 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -216,9 +216,9 @@ type ext_named_context =
   Id.Set.t * named_context
 
 val push_rel_decl_to_named_context :
-  rel_declaration -> ext_named_context -> ext_named_context
+  evar_map -> rel_declaration -> ext_named_context -> ext_named_context
 
-val push_rel_context_to_named_context : Environ.env -> types ->
+val push_rel_context_to_named_context : Environ.env -> evar_map -> types ->
   named_context_val * types * constr list * csubst * (identifier*constr) list
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
diff --git a/engine/namegen.ml b/engine/namegen.ml
index e56ec2877..7b7302957 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -15,12 +15,13 @@
 open Util
 open Names
 open Term
+open Environ
+open EConstr
 open Vars
 open Nametab
 open Nameops
 open Libnames
 open Globnames
-open Environ
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -84,13 +85,20 @@ let is_section_variable id =
 (**********************************************************************)
 (* Generating "intuitive" names from its type *)
 
-let head_name c = (* Find the head constant of a constr if any *)
+let global_of_constr = function
+| Const (c, _) -> ConstRef c
+| Ind (i, _) -> IndRef i
+| Construct (c, _) -> ConstructRef c
+| Var id -> VarRef id
+| _ -> assert false
+
+let head_name sigma c = (* Find the head constant of a constr if any *)
   let rec hdrec c =
-    match kind_of_term c with
+    match EConstr.kind sigma c with
     | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
     | Cast (c,_,_) | App (c,_) -> hdrec c
     | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn)))
-    | Const _ | Ind _ | Construct _ | Var _ ->
+    | Const _ | Ind _ | Construct _ | Var _ as c ->
 	Some (basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
 	Some (match lna.(i) with Name id -> id | _ -> assert false)
@@ -105,9 +113,9 @@ let sort_hdchar = function
   | Prop(_) -> "P"
   | Type(_) -> "T"
 
-let hdchar env c =
+let hdchar env sigma c =
   let rec hdrec k c =
-    match kind_of_term c with
+    match EConstr.kind sigma c with
     | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
     | Cast (c,_,_) | App (c,_) -> hdrec k c
     | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn)))
@@ -119,7 +127,7 @@ let hdchar env c =
     | Rel n ->
 	(if n<=k then "p" (* the initial term is flexible product/function *)
 	 else
-	   try match Environ.lookup_rel (n-k) env with
+	   try match lookup_rel (n-k) env with
 	     | LocalAssum (Name id,_)   | LocalDef (Name id,_,_) -> lowercase_first_char id
 	     | LocalAssum (Anonymous,t) | LocalDef (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
 	   with Not_found -> "y")
@@ -131,41 +139,41 @@ let hdchar env c =
   in
   hdrec 0 c
 
-let id_of_name_using_hdchar env a = function
-  | Anonymous -> Id.of_string (hdchar env a)
+let id_of_name_using_hdchar env sigma a = function
+  | Anonymous -> Id.of_string (hdchar env sigma a)
   | Name id   -> id
 
-let named_hd env a = function
-  | Anonymous -> Name (Id.of_string (hdchar env a))
+let named_hd env sigma a = function
+  | Anonymous -> Name (Id.of_string (hdchar env sigma a))
   | x         -> x
 
-let mkProd_name   env (n,a,b) = mkProd (named_hd env a n, a, b)
-let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b)
+let mkProd_name   env sigma (n,a,b) = mkProd (named_hd env sigma a n, a, b)
+let mkLambda_name env sigma (n,a,b) = mkLambda (named_hd env sigma a n, a, b)
 
 let lambda_name = mkLambda_name
 let prod_name = mkProd_name
 
-let prod_create   env (a,b) = mkProd (named_hd env a Anonymous, a, b)
-let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous, a, b)
+let prod_create   env sigma (a,b) = mkProd (named_hd env sigma a Anonymous, a, b)
+let lambda_create env sigma (a,b) =  mkLambda (named_hd env sigma a Anonymous, a, b)
 
-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 name_assumption env sigma = function
+    | LocalAssum (na,t) -> LocalAssum (named_hd env sigma t na, t)
+    | LocalDef (na,c,t) -> LocalDef (named_hd env sigma c na, c, t)
 
-let name_context env hyps =
+let name_context env sigma hyps =
   snd
     (List.fold_left
        (fun (env,hyps) d ->
-	  let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
+	  let d' = name_assumption env sigma d in (push_rel d' env, d' :: hyps))
        (env,[]) (List.rev hyps))
 
-let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
-let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
+let mkProd_or_LetIn_name env sigma b d = mkProd_or_LetIn (name_assumption env sigma d) b
+let mkLambda_or_LetIn_name env sigma b d = mkLambda_or_LetIn (name_assumption env sigma d) b
 
-let it_mkProd_or_LetIn_name env b hyps =
-  it_mkProd_or_LetIn b (name_context env hyps)
-let it_mkLambda_or_LetIn_name env b hyps =
-  it_mkLambda_or_LetIn b (name_context env hyps)
+let it_mkProd_or_LetIn_name env sigma b hyps =
+  it_mkProd_or_LetIn b (name_context env sigma hyps)
+let it_mkLambda_or_LetIn_name env sigma b hyps =
+  it_mkLambda_or_LetIn b (name_context env sigma hyps)
 
 (**********************************************************************)
 (* Fresh names *)
@@ -185,10 +193,10 @@ let restart_subscript id =
      *** make_ident id (Some 0) *** but compatibility would be lost... *)
     forget_subscript id
 
-let visible_ids (nenv, c) =
+let visible_ids sigma (nenv, c) =
   let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in
-  let rec visible_ids n c = match kind_of_term c with
-  | Const _ | Ind _ | Construct _ | Var _ ->
+  let rec visible_ids n c = match EConstr.kind sigma c with
+  | Const _ | Ind _ | Construct _ | Var _ as c ->
     let (gseen, vseen, ids) = !accu in
     let g = global_of_constr c in
     if not (Refset_env.mem g gseen) then
@@ -218,7 +226,7 @@ let visible_ids (nenv, c) =
       | _ -> ids
       in
       accu := (gseen, vseen, ids)
-  | _ -> Constr.iter_with_binders succ visible_ids n c
+  | _ -> EConstr.iter_with_binders sigma succ visible_ids n c
   in
   let () = visible_ids 1 c in
   let (_, _, ids) = !accu in
@@ -228,9 +236,9 @@ let visible_ids (nenv, c) =
 
 (* 1- Looks for a fresh name for printing in cases pattern *)
 
-let next_name_away_in_cases_pattern env_t na avoid =
+let next_name_away_in_cases_pattern sigma env_t na avoid =
   let id = match na with Name id -> id | Anonymous -> default_dependent_ident in
-  let visible = visible_ids env_t in
+  let visible = visible_ids sigma env_t in
   let bad id = Id.List.mem id avoid || is_constructor id
                                     || Id.Set.mem id visible in
   next_ident_away_from id bad
@@ -292,7 +300,7 @@ let next_name_away_with_default_using_types default na avoid t =
 
 let next_name_away = next_name_away_with_default default_non_dependent_string
 
-let make_all_name_different env =
+let make_all_name_different env sigma =
   (** FIXME: this is inefficient, but only used in printing *)
   let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in
   let sign = named_context_val env in
@@ -300,7 +308,7 @@ let make_all_name_different env =
   let env0 = reset_with_named_context sign env in
   Context.Rel.fold_outside
     (fun decl newenv ->
-       let na = named_hd newenv (RelDecl.get_type decl) (RelDecl.get_name decl) in
+       let na = named_hd newenv sigma (RelDecl.get_type decl) (RelDecl.get_name decl) in
        let id = next_name_away na !avoid in
        avoid := id::!avoid;
        push_rel (RelDecl.set_name (Name id) decl) newenv)
@@ -311,12 +319,12 @@ let make_all_name_different env =
    looks for name of same base with lower available subscript beyond current
    subscript *)
 
-let next_ident_away_for_default_printing env_t id avoid =
-  let visible = visible_ids env_t in
+let next_ident_away_for_default_printing sigma env_t id avoid =
+  let visible = visible_ids sigma env_t in
   let bad id = Id.List.mem id avoid || Id.Set.mem id visible in
   next_ident_away_from id bad
 
-let next_name_away_for_default_printing env_t na avoid =
+let next_name_away_for_default_printing sigma env_t na avoid =
   let id = match na with
   | Name id   -> id
   | Anonymous ->
@@ -324,7 +332,7 @@ let next_name_away_for_default_printing env_t na avoid =
       (* taken into account by the function compute_displayed_name_in; *)
       (* just in case, invent a valid name *)
       default_non_dependent_ident in
-  next_ident_away_for_default_printing env_t id avoid
+  next_ident_away_for_default_printing sigma env_t id avoid
 
 (**********************************************************************)
 (* Displaying terms avoiding bound variables clashes *)
@@ -349,45 +357,45 @@ type renaming_flags =
   | RenamingForGoal
   | RenamingElsewhereFor of (Name.t list * constr)
 
-let next_name_for_display flags =
+let next_name_for_display sigma flags =
   match flags with
-  | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern env_t
+  | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern sigma env_t
   | RenamingForGoal -> next_name_away_in_goal
-  | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t
+  | RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
-let compute_displayed_name_in flags avoid na c =
+let compute_displayed_name_in sigma flags avoid na c =
   match na with
-  | Anonymous when noccurn 1 c ->
+  | Anonymous when noccurn sigma 1 c ->
     (Anonymous,avoid)
   | _ ->
-    let fresh_id = next_name_for_display flags na avoid in
-    let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
+    let fresh_id = next_name_for_display sigma flags na avoid in
+    let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in
     (idopt, fresh_id::avoid)
 
-let compute_and_force_displayed_name_in flags avoid na c =
+let compute_and_force_displayed_name_in sigma flags avoid na c =
   match na with
-  | Anonymous when noccurn 1 c ->
+  | Anonymous when noccurn sigma 1 c ->
     (Anonymous,avoid)
   | _ ->
-    let fresh_id = next_name_for_display flags na avoid in
+    let fresh_id = next_name_for_display sigma flags na avoid in
     (Name fresh_id, fresh_id::avoid)
 
-let compute_displayed_let_name_in flags avoid na c =
-  let fresh_id = next_name_for_display flags na avoid in
+let compute_displayed_let_name_in sigma flags avoid na c =
+  let fresh_id = next_name_for_display sigma flags na avoid in
   (Name fresh_id, fresh_id::avoid)
 
-let rename_bound_vars_as_displayed avoid env c =
+let rename_bound_vars_as_displayed sigma avoid env c =
   let rec rename avoid env c =
-    match kind_of_term c with
+    match EConstr.kind sigma c with
     | Prod (na,c1,c2)  ->
 	let na',avoid' =
-          compute_displayed_name_in
+          compute_displayed_name_in sigma
             (RenamingElsewhereFor (env,c2)) avoid na c2 in
 	mkProd (na', c1, rename avoid' (na' :: env) c2)
     | LetIn (na,c1,t,c2) ->
 	let na',avoid' =
-          compute_displayed_let_name_in
+          compute_displayed_let_name_in sigma
             (RenamingElsewhereFor (env,c2)) avoid na c2 in
 	mkLetIn (na',c1,t, rename avoid' (na' :: env) c2)
     | Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 33ce9a34d..058b1c228 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -11,6 +11,8 @@
 open Names
 open Term
 open Environ
+open Evd
+open EConstr
 
 (*********************************************************************
    Conventional default names *)
@@ -26,27 +28,27 @@ val default_dependent_ident : Id.t     (* "x" *)
 
 val lowercase_first_char : Id.t -> string
 val sort_hdchar : sorts -> string
-val hdchar : env -> types -> string
-val id_of_name_using_hdchar : env -> types -> Name.t -> Id.t
-val named_hd : env -> types -> Name.t -> Name.t
-val head_name : types -> Id.t option
+val hdchar : env -> evar_map -> types -> string
+val id_of_name_using_hdchar : env -> evar_map -> types -> Name.t -> Id.t
+val named_hd : env -> evar_map -> types -> Name.t -> Name.t
+val head_name : evar_map -> types -> Id.t option
 
-val mkProd_name : env -> Name.t * types * types -> types
-val mkLambda_name : env -> Name.t * types * constr -> constr
+val mkProd_name : env -> evar_map -> Name.t * types * types -> types
+val mkLambda_name : env -> evar_map -> Name.t * types * constr -> constr
 
 (** Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
-val prod_name : env -> Name.t * types * types -> types
-val lambda_name : env -> Name.t * types * constr -> constr
+val prod_name : env -> evar_map -> Name.t * types * types -> types
+val lambda_name : env -> evar_map -> Name.t * types * constr -> constr
 
-val prod_create : env -> types * types -> constr
-val lambda_create : env -> types * constr -> constr
-val name_assumption : env -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
-val name_context : env -> Context.Rel.t -> Context.Rel.t
+val prod_create : env -> evar_map -> types * types -> constr
+val lambda_create : env -> evar_map -> types * constr -> constr
+val name_assumption : env -> evar_map -> rel_declaration -> rel_declaration
+val name_context : env -> evar_map -> rel_context -> rel_context
 
-val mkProd_or_LetIn_name : env -> types -> Context.Rel.Declaration.t -> types
-val mkLambda_or_LetIn_name : env -> constr -> Context.Rel.Declaration.t -> constr
-val it_mkProd_or_LetIn_name   : env -> types -> Context.Rel.t -> types
-val it_mkLambda_or_LetIn_name : env -> constr -> Context.Rel.t -> constr
+val mkProd_or_LetIn_name : env -> evar_map -> types -> rel_declaration -> types
+val mkLambda_or_LetIn_name : env -> evar_map -> constr -> rel_declaration -> constr
+val it_mkProd_or_LetIn_name   : env -> evar_map -> types -> rel_context -> types
+val it_mkLambda_or_LetIn_name : env -> evar_map -> constr -> rel_context -> constr
 
 (*********************************************************************
    Fresh names *)
@@ -98,16 +100,16 @@ type renaming_flags =
   | RenamingForGoal (** avoid all globals (as in intro) *)
   | RenamingElsewhereFor of (Name.t list * constr)
 
-val make_all_name_different : env -> env
+val make_all_name_different : env -> evar_map -> env
 
 val compute_displayed_name_in :
-  renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val compute_and_force_displayed_name_in :
-  renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val compute_displayed_let_name_in :
-  renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val rename_bound_vars_as_displayed :
-  Id.t list -> Name.t list -> types -> types
+  evar_map -> Id.t list -> Name.t list -> types -> types
 
 (**********************************************************************)
 (* Naming strategy for arguments in Prop when eliminating inductive types *)
diff --git a/engine/termops.ml b/engine/termops.ml
index ff1a0d9de..d8e712abc 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -115,7 +115,7 @@ let pr_evar_suggested_name evk sigma =
   | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
   | _ ->
       let env = reset_with_named_context evi.evar_hyps (Global.env()) in
-      Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
+      Namegen.id_of_name_using_hdchar env sigma (EConstr.of_constr evi.evar_concl) Anonymous
   in
   let names = EvMap.mapi base_id (undefined_map sigma) in
   let id = EvMap.find evk names in
@@ -316,7 +316,7 @@ let print_env_short env =
     str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
     str "[" ++ pr_sequence pr_rel_decl rc ++ str "]"
 
-let pr_evar_constraints pbs =
+let pr_evar_constraints sigma pbs =
   let pr_evconstr (pbty, env, t1, t2) =
     let env =
       (** We currently allow evar instances to refer to anonymous de
@@ -326,10 +326,10 @@ let pr_evar_constraints pbs =
           stop depending on anonymous variables, they can be used to
           indicate independency. Also, this depends on a strategy for
           naming/renaming. *)
-      Namegen.make_all_name_different env
+      Namegen.make_all_name_different env sigma
     in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-      print_constr_env env Evd.empty (EConstr.of_constr t1) ++ spc () ++
+      print_constr_env env sigma (EConstr.of_constr t1) ++ spc () ++
       str (match pbty with
             | Reduction.CONV -> "=="
             | Reduction.CUMUL -> "<=") ++
@@ -346,7 +346,7 @@ let pr_evar_map_gen with_univs pr_evars sigma =
     if List.is_empty conv_pbs then mt ()
     else
     str "CONSTRAINTS:" ++ brk (0, 1) ++
-      pr_evar_constraints conv_pbs ++ fnl ()
+      pr_evar_constraints sigma conv_pbs ++ fnl ()
   and metas =
     if List.is_empty (Evd.meta_list sigma) then mt ()
     else
diff --git a/engine/termops.mli b/engine/termops.mli
index 512bb05ff..0dd5d96fb 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -288,7 +288,7 @@ val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
 val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds
-val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds
+val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.std_ppcmds
 val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
 val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
   evar_map -> Pp.std_ppcmds
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3077231be..8debc06bb 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -953,6 +953,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
   (* Not "goal_concl_style" means do alpha-conversion avoiding only *)
   (* those goal/section/rel variables that occurs in the subterm under *)
   (* consideration; see namegen.ml for further details *)
+  let t = EConstr.of_constr t in
   let avoid = if goal_concl_style then ids_of_context env else [] in
   let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in
   let vars = vars_of_env env in
@@ -965,6 +966,7 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t =
   extern_constr_gen lax goal_concl_style None env sigma t
 
 let extern_type goal_concl_style env sigma t =
+  let t = EConstr.of_constr t in
   let avoid = if goal_concl_style then ids_of_context env else [] in
   let r = Detyping.detype goal_concl_style avoid env sigma t in
   extern_glob_type (vars_of_env env) r
@@ -1042,14 +1044,16 @@ let rec glob_of_pat env sigma = function
 	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive")
       in
       GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
-  | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (mkFix f) (** FIXME bad env *)
-  | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (mkCoFix c)
+  | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f)) (** FIXME bad env *)
+  | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))
   | PSort s -> GSort (loc,s)
 
 let extern_constr_pattern env sigma pat =
   extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
 
 let extern_rel_context where env sigma sign =
+  let sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign in
+  let where = Option.map EConstr.of_constr where in
   let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
   let a = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) a in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 41e2e4e6f..bac97aa3f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1843,7 +1843,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 		  (add_name match_acc (loc,x)) ((loc,x)::var_acc)
 	      | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
 		let fresh =
-		  Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in
+		  Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
 		canonize_args t tt (fresh::forbidden_names)
 		  ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc)
 	      | _ -> assert false in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7dbd94aa7..549e8e787 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -441,6 +441,7 @@ let notation_constr_of_glob_constr nenv a =
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
 
 let notation_constr_of_constr avoiding t =
+  let t = EConstr.of_constr t in
   let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in
   let nenv = {
     ninterp_var_type = Id.Map.empty;
diff --git a/interp/reserve.ml b/interp/reserve.ml
index a4d4f4027..1565ba4a9 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -107,7 +107,9 @@ let constr_key c =
 
 let revert_reserved_type t =
   try
+    let t = EConstr.Unsafe.to_constr t in
     let reserved = KeyMap.find (constr_key t) !reserve_revtable in
+    let t = EConstr.of_constr t in
     let t = Detyping.detype false [] (Global.env()) Evd.empty t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
         then I've introduced a bug... *)
diff --git a/library/impargs.ml b/library/impargs.ml
index 836568b89..a63264b66 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -228,10 +228,12 @@ let rec is_rigid_head t = match kind_of_term t with
 
 (* calcule la liste des arguments implicites *)
 
-let find_displayed_name_in all avoid na (_,b as envnames_b) =
+let find_displayed_name_in all avoid na (env, b) =
+  let b = EConstr.of_constr b in
+  let envnames_b = (env, b) in
   let flag = RenamingElsewhereFor envnames_b in
-  if all then compute_and_force_displayed_name_in flag avoid na b
-  else compute_displayed_name_in flag avoid na b
+  if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
+  else compute_displayed_name_in Evd.empty flag avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rigid = ref true in
diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml
index 01cff94a8..5d3f6df03 100644
--- a/ltac/evar_tactics.ml
+++ b/ltac/evar_tactics.ml
@@ -88,14 +88,14 @@ let let_evar name typ =
     let env = Proofview.Goal.env gl in
     let sigma = ref sigma in
     let _ = Typing.e_sort_of env sigma typ in
-    let sigma = Sigma.Unsafe.of_evar_map !sigma in
+    let sigma = !sigma in
     let id = match name with
     | Names.Anonymous -> 
-      let typ = EConstr.Unsafe.to_constr typ in
-      let id = Namegen.id_of_name_using_hdchar env typ name in
+      let id = Namegen.id_of_name_using_hdchar env sigma typ name in
       Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
     | Names.Name id -> id
     in
+    let sigma = Sigma.Unsafe.of_evar_map sigma in
     let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
     let tac =
       (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 34159d945..58c5823c5 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -645,8 +645,6 @@ let subst_hole_with_term occ tc t =
 open Tacmach
 
 let hResolve id c occ t =
-  let c = EConstr.Unsafe.to_constr c in
-  let t = EConstr.Unsafe.to_constr t in
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let sigma = Sigma.to_evar_map sigma in
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index ae057b458..828d634d0 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -316,7 +316,7 @@ let rec match_aliases names constr = function
       let args,bnames,body = match_aliases qnames body q in
 	st::args,bnames,body
 
-let detype_ground env c = Detyping.detype false [] env Evd.empty c
+let detype_ground env c = Detyping.detype false [] env Evd.empty (EConstr.of_constr c)
 
 let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
   let et,pinfo =
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index adc4ad8a3..4fe59d755 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -440,7 +440,7 @@ let concl_refiner metas body gls =
       [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
     | (n,typ)::rest ->
 	let _A = subst_meta subst typ in
-	let x = id_of_name_using_hdchar env _A Anonymous in
+	let x = id_of_name_using_hdchar env evd (EConstr.of_constr _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) (EConstr.of_constr _A)) in
@@ -895,7 +895,6 @@ let build_per_info etype casee gls =
   let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in
   let is_dep = dependent (project gls) (EConstr.of_constr casee) concl in
   let hd,args = decompose_app (special_whd gls ctyp) in
-  let ctyp = EConstr.Unsafe.to_constr ctyp in
   let (ind,u) =
     try
       destInd hd
@@ -909,10 +908,11 @@ let build_per_info etype casee gls =
   let params,real_args = List.chop nparams args in
   let abstract_obj c body =
     let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
-    let typ = EConstr.Unsafe.to_constr typ in
-      lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in
+      lambda_create env (project gls) (typ,Termops.subst_term (project gls) (EConstr.of_constr c) body) in
   let pred= List.fold_right abstract_obj
-    real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) concl)) in
+    real_args (lambda_create env (project gls) (ctyp,Termops.subst_term (project gls) (EConstr.of_constr casee) concl)) in
+  let ctyp = EConstr.Unsafe.to_constr ctyp in
+  let pred = EConstr.Unsafe.to_constr pred in
     is_dep,
   {per_casee=casee;
    per_ctype=ctyp;
@@ -1275,16 +1275,15 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let env=pf_env gls in
 	let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in
 	let hd,all_args = decompose_app (special_whd gls ctyp) in
-	let ctyp = EConstr.Unsafe.to_constr ctyp in
 	let ind', u = destInd hd in
 	let _ = assert (eq_ind ind' ind) in (* just in case *)
 	let params,real_args = List.chop nparams all_args in
 	let abstract_obj c body =
 	  let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
-	  let typ = EConstr.Unsafe.to_constr typ in
-	    lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in
+	    lambda_create env (project gls) (typ,Termops.subst_term (project gls) (EConstr.of_constr c) body) in
 	let elim_pred = List.fold_right abstract_obj
-	  real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) concl)) in
+	  real_args (lambda_create env (project gls) (ctyp,Termops.subst_term (project gls) (EConstr.of_constr casee) concl)) in
+        let elim_pred = EConstr.Unsafe.to_constr elim_pred in
 	let case_info = Inductiveops.make_case_info env ind RegularStyle in
 	let gen_arities = Inductive.arities_of_constructors (ind,u) spec in
 	let f_ids typ =
@@ -1345,6 +1344,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 
 let understand_my_constr env sigma c concl =
   let env = env in
+  let c = EConstr.of_constr c in
   let rawc = Detyping.detype false [] env Evd.empty c in
   let rec frob = function
     | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index fd2f4bbd3..63bd3848f 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -421,7 +421,7 @@ let rec pattern_to_term_and_type env typ  = function
 	Array.to_list
 	  (Array.init
 	     (cst_narg - List.length patternl)
-	     (fun i -> Detyping.detype false [] env (Evd.from_env env) csta.(i))
+	     (fun i -> Detyping.detype false [] env (Evd.from_env env) (EConstr.of_constr csta.(i)))
 	  )
       in
       let patl_as_term =
@@ -504,7 +504,6 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		*)
 		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
 		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in
-                let rt_typ = EConstr.Unsafe.to_constr rt_typ in
 		let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
@@ -757,7 +756,6 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			let typ_of_id =
 			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
 			in
-			let typ_of_id = EConstr.Unsafe.to_constr typ_of_id in
 			let raw_typ_of_id =
 			  Detyping.detype false []
 			    env_with_pat_ids (Evd.from_env env) typ_of_id
@@ -804,6 +802,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	      List.map3
 	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in
+		 let typ_as_constr = EConstr.of_constr typ_as_constr in
 		 let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
 		 List.fold_right
@@ -811,7 +810,6 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		      if Id.Set.mem id this_pat_ids
 		      then (Prod (Name id),
 		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
-		      let typ_of_id = EConstr.Unsafe.to_constr typ_of_id in
 		      let raw_typ_of_id =
 			Detyping.detype false [] new_env (Evd.from_env env) typ_of_id
 		      in
@@ -970,7 +968,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			    (List.map
 			      (fun p -> Detyping.detype false []
 				 env (Evd.from_env env)
-				 p) params)@(Array.to_list
+				 (EConstr.of_constr p)) params)@(Array.to_list
 				      (Array.make
 					 (List.length args' - nparam)
 					 (mkGHole ()))))
@@ -988,6 +986,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			    let ty' = snd (Util.List.chop nparam ty) in
 			    List.fold_left2
 			      (fun acc var_as_constr arg ->
+                                let arg = EConstr.of_constr arg in
 				 if isRel var_as_constr
 				 then
 				   let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 691385fad..44aacaf45 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -777,6 +777,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
   let mkrawcor nme avoid typ =
     (* first replace rel 1 by a varname *)
     let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
+    let substindtyp = EConstr.of_constr substindtyp in
     Detyping.detype false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in
   let lcstr1: glob_constr list =
     Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
@@ -860,6 +861,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
 let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
   match rdecl with
     | LocalAssum (nme,t) ->
+        let t = EConstr.of_constr t in
         let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
         GProd (Loc.ghost,nme,Explicit,traw,t2)
     | LocalDef _ -> assert false
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f5ea32878..2a66ba852 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -122,8 +122,8 @@ let pf_get_new_ids idl g =
     []
 
 let compute_renamed_type gls c =
-  EConstr.of_constr (rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
-    (EConstr.Unsafe.to_constr (pf_unsafe_type_of gls c)))
+  rename_bound_vars_as_displayed (project gls) (*no avoid*) [] (*no rels*) []
+    (pf_unsafe_type_of gls c)
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
 let ano_id = Id.of_string "anonymous"
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
diff --git a/printing/printer.ml b/printing/printer.ml
index c7d3a1ba3..447337b9a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -515,7 +515,7 @@ let print_evar_constraints gl sigma =
           problem. MS: we should rather stop depending on anonymous variables, they
           can be used to indicate independency. Also, this depends on a strategy for 
           naming/renaming *)
-      Namegen.make_all_name_different env in
+      Namegen.make_all_name_different env sigma in
     str" " ++
       hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++
              str (match pbty with
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index e580bccc3..5645850b2 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -555,7 +555,7 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
       let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
-      let t = EConstr.of_constr (rename_bound_vars_as_displayed [] [] (EConstr.Unsafe.to_constr t)) in
+      let t = rename_bound_vars_as_displayed sigma [] [] t in
       let clause = mk_clenv_from_env env sigma n
 	(c, t)
       in clenv_match_args lbind clause
@@ -603,9 +603,7 @@ let make_evar_clause env sigma ?len t =
   | Some n -> assert (0 <= n); n
   in
   (** FIXME: do the renaming online *)
-  let t = EConstr.Unsafe.to_constr t in
-  let t = rename_bound_vars_as_displayed [] [] t in
-  let t = EConstr.of_constr t in
+  let t = rename_bound_vars_as_displayed sigma [] [] t in
   let rec clrec (sigma, holes) n t =
     if n = 0 then (sigma, holes, t)
     else match EConstr.kind sigma t with
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 55fda1c7d..669d80814 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1458,7 +1458,7 @@ let _ =
   Hook.set Typeclasses.solve_all_instances_hook solve_inst
 
 let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
-  let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env gl in
+  let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env sigma gl in
   let (gl,t,sigma) =
     Goal.V82.mk_goal sigma nc gl Store.empty in
   let (ev, _) = destEvar sigma t in
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 188e215a5..b08456f2f 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -76,10 +76,24 @@ let build_dependent_inductive ind (mib,mip) =
        Context.Rel.to_extended_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt
        @ Context.Rel.to_extended_list mkRel 0 realargs)
 
+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 name_context env hyps =
+  snd
+    (List.fold_left
+       (fun (env,hyps) d ->
+	  let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
+       (env,[]) (List.rev hyps))
+
 let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
 let my_it_mkProd_or_LetIn s c = Term.it_mkProd_or_LetIn c s
 let my_it_mkLambda_or_LetIn_name s c =
-  it_mkLambda_or_LetIn_name (Global.env()) c s
+  let env = Global.env () in
+  let mkLambda_or_LetIn_name d b = mkLambda_or_LetIn (name_assumption env d) b in
+  List.fold_left (fun c d -> mkLambda_or_LetIn_name d c) c s
 
 let get_coq_eq ctx =
   try
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7f7a07b8f..d9b668517 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -857,14 +857,13 @@ let descend_then env sigma head dirn =
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
-      let deparsign = make_arity_signature env true indf in
-      let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in
+      let deparsign = make_arity_signature env sigma true indf in
       let p =
 	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
       let build_branch i =
 	let result = if Int.equal i dirn then dirnval else dfltval in
-	let args = name_context env cstr.(i-1).cs_args in
-	let args = List.map (fun d -> map_rel_decl EConstr.of_constr d) args in
+	let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.(i-1).cs_args in
+	let args = name_context env sigma cs_args in
 	it_mkLambda_or_LetIn result args in
       let brl =
         List.map build_branch
@@ -905,8 +904,7 @@ let build_selector env sigma dirn c ind special default =
   let ind, _ = check_privacy env indp in
   let typ = Retyping.get_type_of env sigma default in
   let (mib,mip) = lookup_mind_specif env ind in
-  let deparsign = make_arity_signature env true indf in
-  let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in
+  let deparsign = make_arity_signature env sigma true indf in
   let p = it_mkLambda_or_LetIn typ deparsign in
   let cstrs = get_constructors env indf in
   let build_branch i =
@@ -1535,9 +1533,6 @@ let decomp_tuple_term env sigma c t =
     in [((ex,exty),inner_code)]::iterated_decomp
   in decomprec (mkRel 1) c t
 
-let lambda_create env (a,b) =
-  mkLambda (named_hd env (EConstr.Unsafe.to_constr a) Anonymous, a, b)
-
 let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let sigma = Sigma.to_evar_map sigma in
   let typ = get_type_of env sigma dep_pair1 in
@@ -1555,9 +1550,9 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* We build the expected goal *)
   let abst_B =
     List.fold_right
-      (fun (e,t) body -> lambda_create env (t,subst_term sigma e body)) e1_list b in
+      (fun (e,t) body -> lambda_create env sigma (t,subst_term sigma e body)) e1_list b in
   let pred_body = beta_applist sigma (abst_B,proj_list) in
-  let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in
+  let body = mkApp (lambda_create env sigma (typ,pred_body),[|dep_pair1|]) in
   let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
   let expected_goal = nf_betaiota sigma expected_goal in
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ecb8eedac..632a29721 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -90,8 +90,7 @@ let make_inv_predicate env evd indf realargs id status concl =
               | None ->
 		let sort = get_sort_family_of env !evd concl in
 		let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in
-		let p = make_arity env true indf sort in
-		let p = EConstr.of_constr p in
+		let p = make_arity env !evd true indf sort in
 		let evd',(p,ptyp) = Unification.abstract_list_all env
                   !evd p concl (realargs@[mkVar id])
 		in evd := evd'; p in
@@ -133,11 +132,7 @@ let make_inv_predicate env evd indf realargs id status concl =
         build_concl eqns args (succ n) restlist
   in
   let (newconcl, args) = build_concl [] [] 0 realargs in
-  let name_context env ctx =
-    let map f c = List.map (fun d -> Termops.map_rel_decl f d) c in
-    map EConstr.of_constr (name_context env (map EConstr.Unsafe.to_constr ctx))
-  in
-  let predicate = it_mkLambda_or_LetIn newconcl (name_context env hyps) in
+  let predicate = it_mkLambda_or_LetIn newconcl (name_context env !evd hyps) in
   let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in
   (* OK - this predicate should now be usable by res_elimination_then to
      do elimination on the conclusion. *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index d7c396179..d864e547c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -119,11 +119,11 @@ let max_prefix_sign lid sign =
 let rec add_prods_sign env sigma t =
   match EConstr.kind sigma (whd_all env sigma t) with
     | Prod (na,c1,b) ->
-	let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in
+	let id = id_of_name_using_hdchar env sigma t na in
 	let b'= subst1 (mkVar id) b in
         add_prods_sign (push_named (LocalAssum (id,c1)) env) sigma b'
     | LetIn (na,c1,t1,b) ->
-	let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in
+	let id = id_of_name_using_hdchar env sigma t na in
 	let b'= subst1 (mkVar id) b in
         add_prods_sign (push_named (LocalDef (id,c1,t1)) env) sigma b'
     | _ -> (env,t)
@@ -147,8 +147,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
   let p = next_ident_away (Id.of_string "P") allvars in
   let pty,goal =
     if dep_option  then
-      let pty = make_arity env true indf sort in
-      let pty = EConstr.of_constr pty in
+      let pty = make_arity env sigma true indf sort in
       let goal =
 	mkProd
 	  (Anonymous, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a29803251..13ffbc52f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -412,16 +412,13 @@ let id_of_name_with_default id = function
 let default_id_of_sort s =
   if Sorts.is_small s then default_small_ident else default_type_ident
 
-let id_of_name_using_hdchar env c name =
-  id_of_name_using_hdchar env (EConstr.Unsafe.to_constr c) name
-
 let default_id env sigma decl =
   let open Context.Rel.Declaration in
   match decl with
   | LocalAssum (name,t) ->
       let dft = default_id_of_sort (Retyping.get_sort_of env sigma t) in
       id_of_name_with_default dft name
-  | LocalDef (name,b,_) -> id_of_name_using_hdchar env b name
+  | LocalDef (name,b,_) -> id_of_name_using_hdchar env sigma b name
 
 (* Non primitive introduction tactics are treated by intro_then_gen
    There is possibly renaming, with possibly names to avoid and
@@ -1075,14 +1072,14 @@ let intros_replacing ids =
 
 (* User-level introduction tactics *)
 
-let lookup_hypothesis_as_renamed env ccl = function
-  | AnonHyp n -> Detyping.lookup_index_as_renamed env (EConstr.Unsafe.to_constr ccl) n
-  | NamedHyp id -> Detyping.lookup_name_as_displayed env (EConstr.Unsafe.to_constr ccl) id
+let lookup_hypothesis_as_renamed env sigma ccl = function
+  | AnonHyp n -> Detyping.lookup_index_as_renamed env sigma ccl n
+  | NamedHyp id -> Detyping.lookup_name_as_displayed env sigma ccl id
 
 let lookup_hypothesis_as_renamed_gen red h gl =
   let env = Proofview.Goal.env gl in
   let rec aux ccl =
-    match lookup_hypothesis_as_renamed env ccl h with
+    match lookup_hypothesis_as_renamed env (Tacmach.New.project gl) ccl h with
       | None when red ->
         let (redfun, _) = Redexpr.reduction_of_red_expr env (Red true) in
         let Sigma (c, _, _) = redfun.e_redfun env (Proofview.Goal.sigma gl) ccl in
@@ -1350,7 +1347,7 @@ let enforce_prop_bound_names rename tac =
               if Retyping.get_sort_family_of env sigma t = InProp then
                 (* "very_standard" says that we should have "H" names only, but
                    this would break compatibility even more... *)
-                let s = match Namegen.head_name (EConstr.Unsafe.to_constr t) with
+                let s = match Namegen.head_name sigma t with
                   | Some id when not very_standard -> string_of_id id
                   | _ -> "" in
                 Name (add_suffix Namegen.default_prop_ident s)
@@ -2768,7 +2765,7 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t
 
 (* Compute a name for a generalization *)
 
-let generalized_name sigma c t ids cl = function
+let generalized_name env sigma c t ids cl = function
   | Name id as na ->
       if Id.List.mem id ids then
 	user_err  (pr_id id ++ str " is already used.");
@@ -2783,7 +2780,7 @@ let generalized_name sigma c t ids cl = function
 	    (* On ne s'etait pas casse la tete : on avait pris pour nom de
                variable la premiere lettre du type, meme si "c" avait ete une
                constante dont on aurait pu prendre directement le nom *)
-	    named_hd (Global.env()) (EConstr.Unsafe.to_constr t) Anonymous
+	    named_hd env sigma t Anonymous
 
 (* Abstract over [c] in [forall x1:A1(c)..xi:Ai(c).T(c)] producing
    [forall x, x1:A1(x1), .., xi:Ai(x). T(x)] with all [c] abtracted in [Ai]
@@ -2795,7 +2792,7 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
   let dummy_prod = it_mkProd_or_LetIn mkProp decls in
   let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in
   let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in
-  let na = generalized_name sigma c t ids cl' na in
+  let na = generalized_name env sigma c t ids cl' na in
   let decl = match b with
     | None -> LocalAssum (na,t)
     | Some b -> LocalDef (na,b,t)
@@ -3230,7 +3227,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
             | Var id -> id
             | _ ->
             let type_of = Tacmach.New.pf_unsafe_type_of gl in
-            id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
+            id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in
             let x = fresh_id_in_env avoid id env in
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) c None allHypsAndConcl)
@@ -4434,7 +4431,7 @@ let induction_gen clear_flag isrec with_evars elim
      declaring the induction argument as a new local variable *)
     let id =
     (* Type not the right one if partially applied but anyway for internal use*)
-      let x = id_of_name_using_hdchar (Global.env()) t Anonymous in
+      let x = id_of_name_using_hdchar (Global.env()) evd t Anonymous in
       new_fresh_id [] x gl in
     let info_arg = (is_arg_pure_hyp, not enough_applied) in
     pose_induction_arg_then
@@ -4471,7 +4468,7 @@ let induction_gen_l isrec with_evars elim names lc =
                 let type_of = Tacmach.New.pf_unsafe_type_of gl in
                 let sigma = Tacmach.New.project gl in
                 let x =
-		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
+		  id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in
 
                 let id = new_fresh_id [] x gl in
 		let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index 576fbd7c0..c0eede99e 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,13 +6,13 @@ fun e : option L => match e with
      : option L -> option L
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x := A n : T n in ?y ?y0 : T n
+fun n : nat => let x := A n : T n in ?t ?y : T n
      : forall n : nat, T n
 where
-?y : [n : nat  x := A n : T n |- ?T -> T n] 
-?y0 : [n : nat  x := A n : T n |- ?T] 
-fun n : nat => ?y ?y0 : T n
+?t : [n : nat  x := A n : T n |- ?T -> T n] 
+?y : [n : nat  x := A n : T n |- ?T] 
+fun n : nat => ?t ?y : T n
      : forall n : nat, T n
 where
-?y : [n : nat |- ?T -> T n] 
-?y0 : [n : nat |- ?T] 
+?t : [n : nat |- ?T -> T n] 
+?y : [n : nat |- ?T] 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 6982205fd..dea1f22d9 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -39,7 +39,7 @@ let contract env sigma lc =
           env
       | _ ->
           let t = Vars.substl !l (RelDecl.get_type decl) in
-          let decl = decl |> RelDecl.map_name (named_hd env (EConstr.Unsafe.to_constr t)) |> RelDecl.map_value (Vars.substl !l) |> RelDecl.set_type t in
+          let decl = decl |> RelDecl.map_name (named_hd env sigma t) |> RelDecl.map_value (Vars.substl !l) |> RelDecl.set_type t in
           l := (mkRel 1) :: List.map (Vars.lift 1) !l;
           push_rel decl env
   in
@@ -206,7 +206,7 @@ let pr_puniverses f env (c,u) =
 
 let explain_elim_arity env sigma ind sorts c pj okinds =
   let open EConstr in
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let pi = pr_inductive env (fst ind) in
   let pc = pr_leconstr_env env sigma c in
   let msg = match okinds with
@@ -241,7 +241,7 @@ let explain_elim_arity env sigma ind sorts c pj okinds =
 
 let explain_case_not_inductive env sigma cj =
   let cj = Evarutil.j_nf_evar sigma cj in
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let pc = pr_leconstr_env env sigma cj.uj_val in
   let pct = pr_leconstr_env env sigma cj.uj_type in
     match EConstr.kind sigma cj.uj_type with
@@ -254,7 +254,7 @@ let explain_case_not_inductive env sigma cj =
 
 let explain_number_branches env sigma cj expn =
   let cj = Evarutil.j_nf_evar sigma cj in
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let pc = pr_leconstr_env env sigma cj.uj_val in
   let pct = pr_leconstr_env env sigma cj.uj_type in
   str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++
@@ -263,7 +263,7 @@ let explain_number_branches env sigma cj expn =
 
 let explain_ill_formed_branch env sigma c ci actty expty =
   let simp t = Reductionops.nf_betaiota sigma (Evarutil.nf_evar sigma t) in
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let pc = pr_leconstr_env env sigma c in
   let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
   strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
@@ -300,7 +300,7 @@ let explain_unification_error env sigma p1 p2 = function
         (* Error speaks from itself *) []
      | ConversionFailed (env,t1,t2) ->
         if EConstr.eq_constr sigma t1 p1 && EConstr.eq_constr sigma t2 p2 then [] else
-        let env = make_all_name_different env in
+        let env = make_all_name_different env sigma in
         let t1 = Evarutil.nf_evar sigma t1 in
         let t2 = Evarutil.nf_evar sigma t2 in
         if not (EConstr.eq_constr sigma t1 p1) || not (EConstr.eq_constr sigma t2 p2) then
@@ -328,7 +328,7 @@ let explain_unification_error env sigma p1 p2 = function
         let u = EConstr.of_constr u in
         let t = Evarutil.nf_evar sigma t in
         let u = Evarutil.nf_evar sigma u in
-        let env = make_all_name_different env in
+        let env = make_all_name_different env sigma in
         (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++
         str " == " ++ pr_leconstr_env env sigma u)
         :: aux t u e
@@ -341,7 +341,7 @@ let explain_unification_error env sigma p1 p2 = function
             prlist_with_sep pr_semicolon (fun x -> x) l ++ str ")"
 
 let explain_actual_type env sigma j t reason =
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let j = j_nf_betaiotaevar sigma j in
   let t = Reductionops.nf_betaiota sigma t in
   (** Actually print *)
@@ -361,7 +361,7 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
   let exptyp = Evarutil.nf_evar sigma exptyp in
   let actualtyp = Reductionops.nf_betaiota sigma actualtyp in
   let rator = Evarutil.j_nf_evar sigma rator in
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in
   let nargs = Array.length randl in
 (*  let pe = pr_ne_context_of (str "in environment") env sigma in*)
@@ -387,7 +387,7 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
 let explain_cant_apply_not_functional env sigma rator randl =
   let randl = Evarutil.jv_nf_evar sigma randl in
   let rator = Evarutil.j_nf_evar sigma rator in
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let nargs = Array.length randl in
 (*  let pe = pr_ne_context_of (str "in environment") env sigma in*)
   let pr = pr_leconstr_env env sigma rator.uj_val in
@@ -437,7 +437,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
       str "Recursive definition on" ++ spc () ++ pr_lconstr_env env sigma c ++
       spc () ++ str "which should be an inductive type"
   | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) ->
-      let arg_env = make_all_name_different arg_env in
+      let arg_env = make_all_name_different arg_env sigma in
       let called =
         match names.(j) with
             Name id -> pr_id id
@@ -503,7 +503,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
   pr_ne_context_of (str "In environment") env sigma ++
   st ++ str "." ++ fnl () ++
   (try (* May fail with unresolved globals. *)
-      let fixenv = make_all_name_different fixenv in
+      let fixenv = make_all_name_different fixenv sigma in
       let pvd = pr_lconstr_env fixenv sigma vdefj.(i).uj_val in
 	str"Recursive definition is:" ++ spc () ++ pvd ++ str "."
     with e when CErrors.noncritical e -> mt ())
@@ -511,7 +511,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
 let explain_ill_typed_rec_body env sigma i names vdefj vargs =
   let vdefj = Evarutil.jv_nf_evar sigma vdefj in
   let vargs = Array.map (Evarutil.nf_evar sigma) vargs in
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let pvd = pr_leconstr_env env sigma vdefj.(i).uj_val in
   let pvdt, pv = pr_explicit env sigma vdefj.(i).uj_type vargs.(i) in
   str "The " ++
@@ -521,13 +521,13 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs =
   str "while it should be" ++ spc () ++ pv ++ str "."
 
 let explain_cant_find_case_type env sigma c =
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let pe = pr_leconstr_env env sigma c in
   str "Cannot infer the return type of pattern-matching on" ++ ws 1 ++
     pe ++ str "."
 
 let explain_occur_check env sigma ev rhs =
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let pt = pr_leconstr_env env sigma rhs in
   str "Cannot define " ++ pr_existential_key sigma ev ++ str " with term" ++
   brk(1,1) ++ pt ++ spc () ++ str "that would depend on itself."
@@ -624,7 +624,7 @@ let explain_wrong_case_info env (ind,u) ci =
     spc () ++ pc ++ str "."
 
 let explain_cannot_unify env sigma m n e =
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let m = Evarutil.nf_evar sigma m in
   let n = Evarutil.nf_evar sigma n in
   let pm, pn = pr_explicit env sigma m n in
@@ -695,7 +695,7 @@ let explain_unsatisfied_constraints env sigma cst =
     spc () ++ str "(maybe a bugged tactic)."
 
 let explain_type_error env sigma err =
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   match err with
   | UnboundRel n ->
       explain_unbound_rel env sigma n
@@ -774,7 +774,7 @@ let pr_constraints printenv env sigma evars cstrs =
         (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++
             str " : " ++ pr_lconstr_env env' sigma evi.evar_concl ++ fnl ()) l
       in
-      h 0 (pe ++ evs ++ pr_evar_constraints cstrs)
+      h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs)
     else
       let filter evk _ = Evar.Map.mem evk evars in
       pr_evar_map_filter ~with_univs:false filter sigma
@@ -810,7 +810,7 @@ let explain_unsatisfiable_constraints env sigma constr comp =
 
 let explain_pretype_error env sigma err =
   let env = Evardefine.env_nf_betaiotaevar sigma env in
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   match err with
   | CantFindCaseType c -> explain_cant_find_case_type env sigma c
   | ActualTypeNotCoercible (j,t,e) ->
@@ -1210,7 +1210,7 @@ let explain_recursion_scheme_error = function
 
 let explain_bad_pattern env sigma cstr ty =
   let ty = EConstr.to_constr sigma ty in
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let pt = pr_lconstr_env env sigma ty in
   let pc = pr_constructor env cstr in
   str "Found the constructor " ++ pc ++ brk(1,1) ++
@@ -1255,7 +1255,7 @@ let explain_non_exhaustive env pats =
 let explain_cannot_infer_predicate env sigma typs =
   let inj c = EConstr.to_constr sigma c in
   let typs = Array.map_to_list (fun (c1, c2) -> (inj c1, inj c2)) typs in
-  let env = make_all_name_different env in
+  let env = make_all_name_different env sigma in
   let pr_branch (cstr,typ) =
     let cstr,_ = decompose_app cstr in
     str "For " ++ pr_lconstr_env env sigma cstr ++ str ": " ++ pr_lconstr_env env sigma typ
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 55477cbcf..43ffa9ef3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1237,7 +1237,7 @@ let vernac_reserve bl =
     let env = Global.env() in
     let sigma = Evd.from_env env in
     let t,ctx = Constrintern.interp_type env sigma c in
-    let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in
+    let t = Detyping.detype false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in
     let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl