Definining EConstr-based contexts.

This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.

22 files changed, 183 insertions, 263 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3b5662a24..a5a5fe6d2 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -15,12 +15,12 @@ open Names
 open Nameops
 open Term
 open Termops
+open Environ
 open EConstr
 open Vars
 open Namegen
 open Declarations
 open Inductiveops
-open Environ
 open Reductionops
 open Type_errors
 open Glob_term
@@ -38,14 +38,6 @@ open Context.Rel.Declaration
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-let local_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  RelDecl.LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  RelDecl.LocalDef (na, inj b, inj t)
-
 (* Pattern-matching errors *)
 
 type pattern_matching_error =
@@ -150,7 +142,7 @@ type tomatch_status =
   | Pushed of (bool*((constr * tomatch_type) * int list * Name.t))
   | Alias of (bool*(Name.t * constr * (constr * types)))
   | NonDepAlias
-  | Abstract of int * Context.Rel.Declaration.t
+  | Abstract of int * rel_declaration
 
 type tomatch_stack = tomatch_status list
 
@@ -261,7 +253,7 @@ type 'a pattern_matching_problem =
       mat       : 'a matrix;
       caseloc   : Loc.t;
       casestyle : case_style;
-      typing_function: type_constraint -> env -> evar_map ref -> 'a option -> EConstr.unsafe_judgment }
+      typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
 
 (*--------------------------------------------------------------------------*
  * A few functions to infer the inductive type from the patterns instead of *
@@ -331,14 +323,12 @@ let binding_vars_of_inductive sigma = function
 let extract_inductive_data env sigma decl =
   match decl with
   | LocalAssum (_,t) ->
-    let t = EConstr.of_constr t in
     let tmtyp =
       try try_find_ind env sigma t None
       with Not_found -> NotInd (None,t) in
     let tmtypvars = binding_vars_of_inductive sigma tmtyp in
     (tmtyp,tmtypvars)
   | LocalDef (_,_,t) ->
-    let t = EConstr.of_constr t in
     (NotInd (None, t), [])
 
 let unify_tomatch_with_patterns evdref env loc typ pats realnames =
@@ -451,7 +441,7 @@ let remove_current_pattern eqn =
 let push_current_pattern (cur,ty) eqn =
   match eqn.patterns with
     | pat::pats ->
-        let rhs_env = push_rel (local_def (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in
+        let rhs_env = push_rel (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in
 	{ eqn with
             rhs = { eqn.rhs with rhs_env = rhs_env };
 	    patterns = pats }
@@ -553,8 +543,8 @@ let dependencies_in_pure_rhs nargs eqns =
 
 let dependent_decl sigma a =
   function
-  | LocalAssum (na,t) -> dependent sigma a (EConstr.of_constr t)
-  | LocalDef (na,c,t) -> dependent sigma a (EConstr.of_constr t) || dependent sigma a (EConstr.of_constr c)
+  | LocalAssum (na,t) -> dependent sigma a t
+  | LocalDef (na,c,t) -> dependent sigma a t || dependent sigma a c
 
 let rec dep_in_tomatch sigma n = function
   | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch sigma n l
@@ -625,7 +615,7 @@ let relocate_index_tomatch sigma n1 n2 =
       NonDepAlias :: genrec depth rest
   | Abstract (i,d) :: rest ->
       let i = relocate_rel n1 n2 depth i in
-      Abstract (i, RelDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (relocate_index sigma n1 n2 depth (EConstr.of_constr c))) d)
+      Abstract (i, RelDecl.map_constr (fun c -> relocate_index sigma n1 n2 depth c) d)
       :: genrec (depth+1) rest in
   genrec 0
 
@@ -658,7 +648,7 @@ let replace_tomatch sigma n c =
   | NonDepAlias  :: rest ->
       NonDepAlias :: replrec depth rest
   | Abstract (i,d) :: rest ->
-      Abstract (i, RelDecl.map_constr (fun t -> EConstr.Unsafe.to_constr (replace_term sigma n c depth (EConstr.of_constr t))) d)
+      Abstract (i, RelDecl.map_constr (fun t -> replace_term sigma n c depth t) d)
       :: replrec (depth+1) rest in
   replrec 0
 
@@ -683,7 +673,7 @@ let rec liftn_tomatch_stack n depth = function
       NonDepAlias :: liftn_tomatch_stack n depth rest
   | Abstract (i,d)::rest ->
       let i = if i<depth then i else i+n in
-      Abstract (i, RelDecl.map_constr (CVars.liftn n depth) d)
+      Abstract (i, RelDecl.map_constr (liftn n depth) d)
       ::(liftn_tomatch_stack n (depth+1) rest)
 
 let lift_tomatch_stack n = liftn_tomatch_stack n 1
@@ -737,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 t na) avoid))
+	     (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env (EConstr.Unsafe.to_constr t) na) avoid))
 	     d na
 	 in
          (na::l,(out_name na)::avoid))
@@ -1145,7 +1135,7 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
   let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with
   | [], _ -> brs,tomatch,pred,[]
   | n::deps, Abstract (i,d) :: tomatch ->
-      let d = map_constr (fun c -> EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c))) d in
+      let d = map_constr (fun c -> nf_evar evd c) d in
       let is_d = match d with LocalAssum _ -> false | LocalDef _ -> true in
       if is_d || List.exists (fun c -> dependent_decl evd (lift k c) d) tocheck
                  && Array.exists (is_dependent_branch evd k) brs then
@@ -1215,12 +1205,12 @@ let rec generalize_problem names pb = function
   | [] -> pb, []
   | i::l ->
       let pb',deps = generalize_problem names pb l in
-      let d = map_constr (CVars.lift i) (Environ.lookup_rel i pb.env) in
+      let d = map_constr (lift i) (lookup_rel i pb.env) in
       begin match d with
       | LocalDef (Anonymous,_,_) -> pb', deps
       | _ ->
 	 (* for better rendering *)
-	let d = RelDecl.map_type (fun c -> EConstr.Unsafe.to_constr (whd_betaiota !(pb.evdref) (EConstr.of_constr c))) d in
+	let d = RelDecl.map_type (fun c -> whd_betaiota !(pb.evdref) c) d in
         let tomatch = lift_tomatch_stack 1 pb'.tomatch in
         let tomatch = relocate_index_tomatch !(pb.evdref) (i+1) 1 tomatch in
         { pb' with
@@ -1247,6 +1237,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   (* build the name x1..xn from the names present in the equations *)
   (* 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 typs = List.map2 RelDecl.set_name names cs_args
   in
@@ -1259,7 +1250,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   (* We adjust the terms to match in the context they will be once the *)
   (* context [x1:T1,..,xn:Tn] will have been pushed on the current env *)
   let typs' =
-    List.map_i (fun i d -> (mkRel i, map_constr (CVars.lift i) d)) 1 typs in
+    List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 typs in
 
   let extenv = push_rel_context typs pb.env in
 
@@ -1415,7 +1406,7 @@ and shift_problem ((current,t),_,na) pb =
   let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in
   let pb =
     { pb with
-       env = push_rel (local_def (na,current,ty)) pb.env;
+       env = push_rel (LocalDef (na,current,ty)) pb.env;
        tomatch = tomatch;
        pred = lift_predicate 1 pred tomatch;
        history = pop_history pb.history;
@@ -1463,7 +1454,7 @@ and compile_generalization pb i d rest =
    ([false]). *)
 and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
   let f c t =
-    let alias = local_def (na,c,t) in
+    let alias = LocalDef (na,c,t) in
     let pb =
       { pb with
          env = push_rel alias pb.env;
@@ -1601,7 +1592,7 @@ let adjust_to_extended_env_and_remove_deps env extenv sigma subst t =
     let (p, _, _) = lookup_rel_id x (rel_context extenv) in
     let rec traverse_local_defs p =
       match lookup_rel p extenv with
-      | LocalDef (_,c,_) -> assert (isRel sigma (EConstr.of_constr c)); traverse_local_defs (p + destRel sigma (EConstr.of_constr c))
+      | LocalDef (_,c,_) -> assert (isRel sigma c); traverse_local_defs (p + destRel sigma c)
       | LocalAssum _ -> p in
     let p = traverse_local_defs p in
     let u = lift (n' - n) u in
@@ -1743,6 +1734,7 @@ let build_inversion_problem loc env sigma tms t =
 	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 patl = pat :: List.rev patl in
 	let patl,sign = recover_and_adjust_alias_names patl sign in
 	let p = List.length patl in
@@ -1751,7 +1743,7 @@ let build_inversion_problem loc env sigma tms t =
 	List.rev_append patl patl',acc_sign,acc
     | (t, NotInd (bo,typ)) :: tms ->
       let pat,acc = make_patvar t acc in
-      let d = local_assum (alias_of_pat pat,typ) in
+      let d = LocalAssum (alias_of_pat pat,typ) in
       let patl,acc_sign,acc = aux (n+1) (push_rel d env) (d::acc_sign) tms acc in
       pat::patl,acc_sign,acc in
   let avoid0 = ids_of_context env in
@@ -1768,7 +1760,7 @@ let build_inversion_problem loc env sigma tms t =
   let n = List.length sign in
 
   let decls =
-    List.map_i (fun i d -> (mkRel i, map_constr (CVars.lift i) d)) 1 sign in
+    List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 sign in
 
   let pb_env = push_rel_context sign env in
   let decls =
@@ -1855,8 +1847,8 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
       | NotInd (bo,typ) ->
 	  (match t with
 	    | None -> (match bo with
-		       | None -> [local_assum (na, lift n typ)]
-		       | Some b -> [local_def (na, lift n b, lift n typ)])
+		       | None -> [LocalAssum (na, lift n typ)]
+		       | Some b -> [LocalDef (na, lift n b, lift n typ)])
 	    | Some (loc,_,_) ->
  	    user_err ~loc 
                 (str"Unexpected type annotation for a term of non inductive type."))
@@ -1865,6 +1857,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 	  let ((ind,u),_) = dest_ind_family indf' in
 	  let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in
 	  let arsign = fst (get_arity env0 indf') in
+	  let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in
 	  let realnal =
 	    match t with
 	      | Some (loc,ind',realnal) ->
@@ -1874,7 +1867,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 		      anomaly (Pp.str "Ill-formed 'in' clause in cases");
 		  List.rev realnal
 	      | None -> List.make nrealargs_ctxt Anonymous in
-	  LocalAssum (na, build_dependent_inductive env0 indf')
+	  LocalAssum (na, EConstr.of_constr (build_dependent_inductive env0 indf'))
 	  ::(List.map2 RelDecl.set_name realnal arsign) in
   let rec buildrec n = function
     | [],[] -> []
@@ -2069,7 +2062,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	      let previd, id = prime avoid (Name (Id.of_string "wildcard")) in
 		Name id, id :: avoid
 	in
-	  (PatVar (l, name), [local_assum (name, ty)] @ realargs, mkRel 1, ty,
+	  (PatVar (l, name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty,
 	   (List.map (fun x -> mkRel 1) realargs), 1, avoid)
     | PatCstr (l,((_, i) as cstr),args,alias) ->
 	let cind = inductive_of_constructor cstr in
@@ -2110,7 +2103,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	      Anonymous ->
 		pat', sign, app, apptype, realargs, n, avoid
 	    | Name id ->
-		let sign = local_assum (alias, lift m ty) :: sign in
+		let sign = LocalAssum (alias, lift m ty) :: sign in
 		let avoid = id :: avoid in
 		let sign, i, avoid =
 		  try
@@ -2122,14 +2115,14 @@ let constr_of_pat env evdref arsign pat avoid =
 		      (lift 1 app) (* aliased term *)
 		    in
 		    let neq = eq_id avoid id in
-		      local_def (Name neq, mkRel 0, eq_t) :: sign, 2, neq :: avoid
+		      LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, neq :: avoid
 		  with Reduction.NotConvertible -> sign, 1, avoid
 		in
 		  (* Mark the equality as a hole *)
 		  pat', sign, lift i app, lift i apptype, realargs, n + i, avoid
   in
-  let pat', sign, patc, patty, args, z, avoid = typ env (EConstr.of_constr (RelDecl.get_type (List.hd arsign)), List.tl arsign) pat avoid in
-    pat', (sign, patc, (EConstr.of_constr (RelDecl.get_type (List.hd arsign)), args), pat'), avoid
+  let pat', sign, patc, patty, args, z, avoid = typ env (RelDecl.get_type (List.hd arsign), List.tl arsign) pat avoid in
+    pat', (sign, patc, (RelDecl.get_type (List.hd arsign), args), pat'), avoid
 
 
 (* shadows functional version *)
@@ -2147,14 +2140,14 @@ match EConstr.kind sigma t with
 let rels_of_patsign sigma =
   List.map (fun decl ->
 	    match decl with
-	    | LocalDef (na,t',t) when is_topvar sigma (EConstr.of_constr t') -> LocalAssum (na,t)
+	    | LocalDef (na,t',t) when is_topvar sigma t' -> LocalAssum (na,t)
 	    | _ -> decl)
 
 let vars_of_ctx sigma ctx =
   let _, y =
     List.fold_right (fun decl (prev, vars) ->
       match decl with
-	| LocalDef (na,t',t) when is_topvar sigma (EConstr.of_constr t') ->
+	| LocalDef (na,t',t) when is_topvar sigma t' ->
 	    prev,
 	    (GApp (Loc.ghost,
 		(GRef (Loc.ghost, delayed_force coq_eq_refl_ref, None)), 
@@ -2174,6 +2167,9 @@ let rec is_included x y =
 	if Int.equal i i' then List.for_all2 is_included args args'
 	else false
 
+let lift_rel_context n l =
+  map_rel_context_with_binders (liftn n) l
+
 (* liftsign is the current pattern's complete signature length. 
    Hence pats is already typed in its
    full signature. However prevpatterns are in the original one signature per pattern form.
@@ -2269,7 +2265,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	     match ineqs with
 	     | None -> [], arity
 	     | Some ineqs ->
-		 [local_assum (Anonymous, ineqs)], lift 1 arity
+		 [LocalAssum (Anonymous, ineqs)], lift 1 arity
 	   in
 	   let eqs_rels, arity = decompose_prod_n_assum !evdref neqs arity in
 	     eqs_rels @ neqs_rels @ rhs_rels', arity
@@ -2280,7 +2276,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
 	 let _btype = evd_comb1 (Typing.type_of env) evdref bbody in
 	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
-	 let branch_decl = local_def (Name branch_name, lift !i bbody, lift !i btype) in
+	 let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in
 	 let branch =
 	   let bref = GVar (Loc.ghost, branch_name) in
 	     match vars_of_ctx !evdref rhs_rels with
@@ -2329,7 +2325,7 @@ let abstract_tomatch env sigma tomatchs tycon =
 		 (fun t -> subst_term sigma (lift 1 c) (lift 1 t)) tycon in
 	       let name = next_ident_away (Id.of_string "filtered_var") names in
 		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
-	       local_def (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx,
+	       LocalDef (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx,
 	       name :: names, tycon)
       ([], [], [], tycon) tomatchs
   in List.rev prev, ctx, tycon
@@ -2356,14 +2352,12 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
 	     let app_decl = List.hd arsign in (* The matched argument *)
 	     let appn = RelDecl.get_name app_decl in
 	     let appt = RelDecl.get_type app_decl in
-	     let appt = EConstr.of_constr appt in
 	     let argsign = List.rev argsign in (* arguments in application order *)
 	     let env', nargeqs, argeqs, refl_args, slift, argsign' =
 	       List.fold_left2
 		 (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg decl ->
 		    let name = RelDecl.get_name decl in
 		    let t = RelDecl.get_type decl in
-		    let t = EConstr.of_constr t in
 		    let argt = Retyping.get_type_of env !evdref arg in
 		    let eq, refl_arg =
 		      if Reductionops.is_conv env !evdref argt t then
@@ -2387,7 +2381,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
 			make_prime avoid name
 		    in
 		      (env, succ nargeqs,
-		       (local_assum (Name (eq_id avoid previd), eq)) :: argeqs,
+		       (LocalAssum (Name (eq_id avoid previd), eq)) :: argeqs,
 		       refl_arg :: refl_args,
 		       pred slift,
 		       RelDecl.set_name (Name id) decl :: argsign'))
@@ -2401,7 +2395,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
 	     in
 	     let refl_eq = mk_JMeq_refl evdref ty tm in
 	     let previd, id = make_prime avoid appn in
-	       ((local_assum (Name (eq_id avoid previd), eq) :: argeqs) :: eqs,
+	       ((LocalAssum (Name (eq_id avoid previd), eq) :: argeqs) :: eqs,
 		succ nargeqs,
 		refl_eq :: refl_args,
 		pred slift,
@@ -2417,7 +2411,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
 	       mk_eq evdref (lift nar tomatch_ty)
 		 (mkRel slift) (lift nar tm)
 	     in
-	       ([local_assum (Name (eq_id avoid previd), eq)] :: eqs, succ neqs,
+	       ([LocalAssum (Name (eq_id avoid previd), eq)] :: eqs, succ neqs,
 		(mk_eq_refl evdref tomatch_ty tm) :: refl_args,
 		pred slift, (arsign' :: []) :: arsigns))
       ([], 0, [], nar, []) tomatchs arsign
@@ -2491,9 +2485,9 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
   (* We push the initial terms to match and push their alias to rhs' envs *)
   (* names of aliases will be recovered from patterns (hence Anonymous here) *)
 
-  let out_tmt na = function NotInd (None,t) -> local_assum (na,t)
-			  | NotInd (Some b, t) -> local_def (na,b,t)
-			  | IsInd (typ,_,_) -> local_assum (na,typ) in
+  let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t)
+			  | NotInd (Some b, t) -> LocalDef (na,b,t)
+			  | IsInd (typ,_,_) -> LocalAssum (na,typ) in
   let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
     
   let typs =
@@ -2566,9 +2560,9 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
     (* names of aliases will be recovered from patterns (hence Anonymous *)
     (* here) *)
 
-    let out_tmt na = function NotInd (None,t) -> local_assum (na,t)
-			    | NotInd (Some b,t) -> local_def (na,b,t)
-			    | IsInd (typ,_,_) -> local_assum (na,typ) in
+    let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t)
+			    | NotInd (Some b,t) -> LocalDef (na,b,t)
+			    | IsInd (typ,_,_) -> LocalAssum (na,typ) in
     let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
 
     let typs =
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 9f26ae9ce..3df2d6873 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -47,11 +47,11 @@ val compile_cases :
 val constr_of_pat : 
            Environ.env ->
            Evd.evar_map ref ->
-           Context.Rel.Declaration.t list ->
+           rel_context ->
            Glob_term.cases_pattern ->
            Names.Id.t list ->
            Glob_term.cases_pattern *
-           (Context.Rel.Declaration.t list * constr *
+           (rel_context * constr *
             (types * constr list) * Glob_term.cases_pattern) *
            Names.Id.t list
 
@@ -85,7 +85,7 @@ type tomatch_status =
   | Pushed of (bool*((constr * tomatch_type) * int list * Name.t))
   | Alias of (bool * (Name.t * constr * (constr * types)))
   | NonDepAlias
-  | Abstract of int * Context.Rel.Declaration.t
+  | Abstract of int * rel_declaration
 
 type tomatch_stack = tomatch_status list
 
@@ -119,6 +119,6 @@ val prepare_predicate :            Loc.t ->
            Environ.env ->
            Evd.evar_map ->
            (types * tomatch_type) list ->
-           Context.Rel.t list ->
+           rel_context list ->
            constr option ->
            'a option -> (Evd.evar_map * Names.name list * constr) list
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 91f53a886..8794f238b 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -18,10 +18,10 @@ open CErrors
 open Util
 open Names
 open Term
+open Environ
 open EConstr
 open Vars
 open Reductionops
-open Environ
 open Typeops
 open Pretype_errors
 open Classops
@@ -127,10 +127,6 @@ let lift_args n sign =
   in
     liftrec (List.length sign) sign
 
-let local_assum (na, t) =
-  let open Context.Rel.Declaration in
-  LocalAssum (na, EConstr.Unsafe.to_constr t)
-
 let mu env evdref t =
   let rec aux v =
     let v' = hnf env !evdref v in
@@ -159,7 +155,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr)
     let subco () = subset_coerce env evdref x y in
     let dest_prod c =
       match Reductionops.splay_prod_n env (!evdref) 1 c with
-      | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na, EConstr.of_constr t), c
+      | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na, t), c
       | _ -> raise NoSubtacCoercion
     in
     let coerce_application typ typ' c c' l l' =
@@ -212,7 +208,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 	  let name' = 
 	    Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.ids_of_context env))
 	  in
-	  let env' = push_rel (local_assum (name', a')) env in
+	  let env' = push_rel (LocalAssum (name', a')) env in
 	  let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
 	    (* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
 	  let coec1 = app_opt env' evdref c1 (mkRel 1) in
@@ -260,7 +256,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 		       | _ -> raise NoSubtacCoercion
 		     in
 		     let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in
-		     let env' = push_rel (local_assum (Name Namegen.default_dependent_ident, a)) env in
+		     let env' = push_rel (LocalAssum (Name Namegen.default_dependent_ident, a)) env in
 		     let c2 = coerce_unify env' b b' in
 		       match c1, c2 with
 		       | None, None -> None
@@ -489,7 +485,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
 	    | Anonymous -> Name Namegen.default_dependent_ident
 	    | _ -> name in
 	  let open Context.Rel.Declaration in
-	  let env1 = push_rel (local_assum (name,u1)) env in
+	  let env1 = push_rel (LocalAssum (name,u1)) env in
 	  let (evd', v1) =
 	    inh_conv_coerce_to_fail loc env1 evd rigidonly
               (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 55612aa66..cad21543b 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -136,14 +136,6 @@ let make_renaming ids = function
   end
 | _ -> dummy_constr
 
-let local_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 let to_fix (idx, (nas, cs, ts)) =
   let inj = EConstr.of_constr in
   (idx, (nas, Array.map inj cs, Array.map inj ts))
@@ -273,15 +265,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
           sorec ctx env subst c1 c2
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
-	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (local_assum (na2,c2)) env)
+	  sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
-	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (local_assum (na2,c2)) env)
+	  sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
-	  sorec ((na1,na2,t2)::ctx) (Environ.push_rel (local_def (na2,c2,t2)) env)
+	  sorec ((na1,na2,t2)::ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
@@ -290,12 +282,12 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
 	  let n = Context.Rel.length ctx_b2 in
           let n' = Context.Rel.length ctx_b2' in
 	  if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then
-            let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,EConstr.of_constr t)::l in
+            let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,t)::l in
 	    let ctx_br = List.fold_left f ctx ctx_b2 in
 	    let ctx_br' = List.fold_left f ctx ctx_b2' in
 	    let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
-	    sorec ctx_br' (Environ.push_rel_context ctx_b2' env)
-	      (sorec ctx_br (Environ.push_rel_context ctx_b2 env)
+	    sorec ctx_br' (push_rel_context ctx_b2' env)
+	      (sorec ctx_br (push_rel_context ctx_b2 env)
                  (sorec ctx env subst a1 a2) b1 b2) b1' b2'
           else
             raise PatternMatchingFailure
@@ -388,21 +380,21 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
       | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2))
       | _ -> assert false
       in
-      let env' = Environ.push_rel (local_assum (x,c1)) env in
+      let env' = EConstr.push_rel (LocalAssum (x,c1)) env in
       try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | Prod (x,c1,c2) ->
       let next_mk_ctx = function
       | [c1; c2] -> mk_ctx (mkProd (x, c1, c2))
       | _ -> assert false
       in
-      let env' = Environ.push_rel (local_assum (x,c1)) env in
+      let env' = EConstr.push_rel (LocalAssum (x,c1)) env in
       try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | LetIn (x,c1,t,c2) ->
       let next_mk_ctx = function
       | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2))
       | _ -> assert false
       in
-      let env' = Environ.push_rel (local_def (x,c1,t)) env in
+      let env' = EConstr.push_rel (LocalDef (x,c1,t)) env in
       try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | App (c1,lc) ->
         let topdown = true in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3ae2e35e6..f5cab070e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -11,12 +11,12 @@ open Util
 open Names
 open Term
 open Termops
+open Environ
 open EConstr
 open Vars
 open CClosure
 open Reduction
 open Reductionops
-open Environ
 open Recordops
 open Evarutil
 open Evardefine
@@ -58,12 +58,12 @@ let eval_flexible_term ts env evd c =
   | Rel n ->
       (try match lookup_rel n env with
            | RelDecl.LocalAssum _ -> None
-           | RelDecl.LocalDef (_,v,_) -> Some (lift n (EConstr.of_constr v))
+           | RelDecl.LocalDef (_,v,_) -> Some (lift n v)
        with Not_found -> None)
   | Var id ->
       (try
 	 if is_transparent_variable ts id then
-	   Option.map EConstr.of_constr (env |> lookup_named id |> NamedDecl.get_value)
+	   env |> lookup_named id |> NamedDecl.get_value
 	 else None
        with Not_found -> None)
   | LetIn (_,b,_,c) -> Some (subst1 b c)
@@ -404,7 +404,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
   let eta env evd onleft sk term sk' term' =
     assert (match sk with [] -> true | _ -> false);
     let (na,c1,c'1) = destLambda evd term in
-    let c = EConstr.to_constr evd c1 in
+    let c = nf_evar evd c1 in
     let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
     let out1 = whd_betaiota_deltazeta_for_iota_state
       (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
@@ -612,8 +612,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
                 (fun i -> evar_conv_x ts env i CUMUL t2 t1)]);
              (fun i -> evar_conv_x ts env i CONV b1 b2);
 	     (fun i ->
-	       let b = EConstr.to_constr i b1 in
-	       let t = EConstr.to_constr i t1 in
+	       let b = nf_evar i b1 in
+	       let t = nf_evar i t1 in
                let na = Nameops.name_max na1 na2 in
 	       evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
@@ -730,7 +730,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
         ise_and evd
           [(fun i -> evar_conv_x ts env i CONV c1 c2);
            (fun i ->
-	     let c = EConstr.to_constr i c1 in
+	     let c = nf_evar i c1 in
              let na = Nameops.name_max na1 na2 in
 	     evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)]
 
@@ -789,7 +789,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
             ise_and evd
               [(fun i -> evar_conv_x ts env i CONV c1 c2);
                (fun i ->
- 	         let c = EConstr.to_constr i c1 in
+ 	         let c = nf_evar i c1 in
                  let na = Nameops.name_max n1 n2 in
 	         evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)]
 
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 5831d3191..faf34baf7 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -11,10 +11,10 @@ open Pp
 open Names
 open Term
 open Termops
+open Environ
 open EConstr
 open Vars
 open Namegen
-open Environ
 open Evd
 open Evarutil
 open Pretype_errors
@@ -22,25 +22,20 @@ open Sigma.Notations
 
 module RelDecl = Context.Rel.Declaration
 
-let nlocal_assum (na, t) =
-  let open Context.Named.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
 let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
   let evd = Sigma.Unsafe.of_evar_map evd in
   let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
   (Sigma.to_evar_map evd, evk)
 
 let env_nf_evar sigma env =
-  let nf_evar c = EConstr.Unsafe.to_constr (nf_evar sigma (EConstr.of_constr c)) in
+  let nf_evar c = nf_evar sigma c in
   process_rel_context
     (fun d e -> push_rel (RelDecl.map_constr nf_evar d) e) env
 
 let env_nf_betaiotaevar sigma env =
   process_rel_context
     (fun d e ->
-      push_rel (RelDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (Reductionops.nf_betaiota sigma (EConstr.of_constr c))) d) e) env
+      push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota sigma c) d) e) env
 
 (****************************************)
 (* Operations on value/type constraints *)
@@ -93,7 +88,7 @@ let define_pure_evar_as_product evd evk =
     (Sigma.to_evar_map evd1, e)
   in
   let evd2,rng =
-    let newenv = push_named (nlocal_assum (id, dom)) evenv in
+    let newenv = push_named (LocalAssum (id, dom)) evenv in
     let src = evar_source evk evd1 in
     let filter = Filter.extend 1 (evar_filter evi) in
       if is_prop_sort s then
@@ -146,7 +141,7 @@ let define_pure_evar_as_lambda env evd evk =
   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
-  let newenv = push_named (nlocal_assum (id, dom)) evenv 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
   let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3235c2505..ff4736528 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -23,14 +23,6 @@ open Evarutil
 open Pretype_errors
 open Sigma.Notations
 
-let nlocal_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  Context.Named.Declaration.LocalAssum (na, inj t)
-
-let nlocal_def (na, b, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  Context.Named.Declaration.LocalDef (na, inj b, inj t)
-
 let normalize_evar evd ev =
   match EConstr.kind evd (mkEvar ev) with
   | Evar (evk,args) -> (evk,args)
@@ -264,7 +256,6 @@ let compute_var_aliases sign sigma =
     let id = get_id decl in
     match decl with
     | LocalDef (_,t,_) ->
-        let t = EConstr.of_constr t in
         (match EConstr.kind sigma t with
         | Var id' ->
             let aliases_of_id =
@@ -281,8 +272,6 @@ let compute_rel_aliases var_aliases rels sigma =
 	  (n-1,
 	   match decl with
 	   | LocalDef (_,t,u) ->
-              let t = EConstr.of_constr t in
-              let u = EConstr.of_constr u in
 	      (match EConstr.kind sigma t with
 	       | Var id' ->
 		  let aliases_of_n =
@@ -338,7 +327,6 @@ let extend_alias sigma decl (var_aliases,rel_aliases) =
   let rel_aliases =
     match decl with
     | LocalDef(_,t,_) ->
-        let t = EConstr.of_constr t in
         (match EConstr.kind sigma t with
         | Var id' ->
             let aliases_of_binder =
@@ -530,7 +518,7 @@ let solve_pattern_eqn env sigma l c =
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
           let open Context.Rel.Declaration in
-          let d = map_constr (CVars.lift n) (lookup_rel n env) in
+          let d = map_constr (lift n) (lookup_rel n env) in
           mkLambda_or_LetIn d c'
       | Var id ->
           let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
@@ -556,6 +544,7 @@ let solve_pattern_eqn env sigma l c =
 
 let make_projectable_subst aliases sigma evi args =
   let sign = evar_filtered_context evi in
+  let sign = List.map (fun d -> map_named_decl EConstr.of_constr d) sign in
   let evar_aliases = compute_var_aliases sign sigma in
   let (_,full_subst,cstr_subst) =
     List.fold_right
@@ -571,7 +560,7 @@ let make_projectable_subst aliases sigma evi args =
               | _ -> cstrs in
             (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs)
         | LocalDef (id,c,_), a::rest ->
-            (match EConstr.kind sigma (EConstr.of_constr c) with
+            (match EConstr.kind sigma c with
             | Var id' ->
                 let idc = normalize_alias_var sigma evar_aliases id' in
                 let sub = try Id.Map.find idc all with Not_found -> [] in
@@ -646,19 +635,17 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       let LocalAssum (na,t_in_env) | LocalDef (na,_,t_in_env) = d in
       let id = next_name_away na avoid in
       let evd,t_in_sign =
-        let t_in_env = EConstr.of_constr t_in_env in
         let s = Retyping.get_sort_of env evd t_in_env in
         let evd,ty_t_in_sign = refresh_universes
 	 ~status:univ_flexible (Some false) env evd (mkSort s) in
         define_evar_from_virtual_equation define_fun env evd src t_in_env
           ty_t_in_sign sign filter inst_in_env in
       let evd,d' = match d with
-      | LocalAssum _ -> evd, nlocal_assum (id,t_in_sign)
+      | LocalAssum _ -> evd, Context.Named.Declaration.LocalAssum (id,t_in_sign)
       | LocalDef (_,b,_) ->
-          let b = EConstr.of_constr b in
           let evd,b = define_evar_from_virtual_equation define_fun env evd src b
             t_in_sign sign filter inst_in_env in
-          evd, nlocal_def (id,b,t_in_sign) in
+          evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in
       (push_named_context_val d' sign, Filter.extend 1 filter,
        (mkRel 1)::(List.map (lift 1) inst_in_env),
        (mkRel 1)::(List.map (lift 1) inst_in_sign),
@@ -1238,9 +1225,11 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar
 	 The body of ?X and ?Y just has to be of type Π Δ. Type k for some k <= i, j. *)
       let evienv = Evd.evar_env evi in
       let ctx1, i = Reduction.dest_arity evienv evi.evar_concl in
+      let ctx1 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx1 in
       let evi2 = Evd.find evd evk2 in
       let evi2env = Evd.evar_env evi2 in
       let ctx2, j = Reduction.dest_arity evi2env evi2.evar_concl in
+      let ctx2 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx2 in
       let ui, uj = univ_of_sort i, univ_of_sort j in
 	if i == j || Evd.check_eq evd ui uj
 	then (* Shortcut, i = j *) 
@@ -1397,7 +1386,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           (* No unique projection but still restrict to where it is possible *)
           (* materializing is necessary, but is restricting useful? *)
           let ty = find_solution_type (evar_filtered_env evi) sols in
-          let ty' = instantiate_evar_array evi (EConstr.of_constr ty) argsv in
+          let ty' = instantiate_evar_array evi ty argsv in
           let (evd,evar,(evk',argsv' as ev')) =
             materialize_evar (evar_define conv_algo ~choose) env !evdref 0 ev ty' in
           let ts = expansions_of_var evd aliases t in
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index d09686f6e..3fc569fc4 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -64,8 +64,8 @@ let proceed_with_occurrences f occs x =
 let map_named_declaration_with_hyploc f hyploc acc decl =
   let open Context.Named.Declaration in
   let f acc typ =
-    let acc, typ = f (Some (NamedDecl.get_id decl, hyploc)) acc (EConstr.of_constr typ) in
-    acc, EConstr.Unsafe.to_constr typ
+    let acc, typ = f (Some (NamedDecl.get_id decl, hyploc)) acc typ in
+    acc, typ
   in
   match decl,hyploc with
   | LocalAssum (id,_), InHypValueOnly ->
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 3d2ebb72d..e3d3b74f1 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -51,7 +51,7 @@ val replace_term_occ_decl_modulo :
   evar_map ->
   (occurrences * hyp_location_flag) or_like_first ->
   'a testing_function -> (unit -> constr) ->
-  Context.Named.Declaration.t -> Context.Named.Declaration.t
+  named_declaration -> named_declaration
 
 (** [subst_closed_term_occ occl c d] replaces occurrences of
     closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
@@ -63,7 +63,7 @@ val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
     closed [c] at positions [occl] by [Rel 1] in [decl]. *)
 val subst_closed_term_occ_decl : env -> evar_map ->
   (occurrences * hyp_location_flag) or_like_first ->
-  constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map
+  constr -> named_declaration -> named_declaration * evar_map
 
 (** Miscellaneous *)
 val error_invalid_occurrence : int list -> 'a
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index c00ceb02e..3191a58ff 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -371,7 +371,7 @@ let make_case_or_project env sigma indf ci pred c branches =
 	  | LocalAssum (na, t) ->
 	     let t = mkProj (Projection.make ps.(i) true, c) in
 	     (i + 1, t :: subst)
-	  | LocalDef (na, b, t) -> (i, Vars.substl subst (EConstr.of_constr b) :: subst))
+	  | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
 	 ctx (0, [])
      in Vars.substl subst br
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 26e23be23..954aa6a94 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -121,19 +121,10 @@ let head_of_constr_reference sigma c = match EConstr.kind sigma c with
   | Var id -> VarRef id
   | _ -> anomaly (Pp.str "Not a rigid reference")
 
-let local_assum (na, t) =
-  let open Context.Rel.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let open Context.Rel.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 let pattern_of_constr env sigma t =
   let open EConstr in
   let rec pattern_of_constr env t =
+  let open Context.Rel.Declaration in
   match EConstr.kind sigma t with
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
@@ -143,11 +134,11 @@ let pattern_of_constr env sigma t =
     | Sort (Type _) -> PSort (GType [])
     | Cast (c,_,_)      -> pattern_of_constr env c
     | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,
-				  pattern_of_constr (push_rel (local_def (na,c,t)) env) b)
+				  pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b)
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr env c,
-				pattern_of_constr (push_rel (local_assum (na, c)) env) b)
+				pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
     | Lambda (na,c,b) -> PLambda (na,pattern_of_constr env c,
-				  pattern_of_constr (push_rel (local_assum (na, c)) env) b)
+				  pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
     | App (f,a) ->
         (match
           match EConstr.kind sigma f with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4660978df..2470decdd 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -28,10 +28,10 @@ open Names
 open Evd
 open Term
 open Termops
+open Environ
 open EConstr
 open Vars
 open Reductionops
-open Environ
 open Type_errors
 open Typeops
 open Typing
@@ -70,16 +70,6 @@ open Inductiveops
 
 (************************************************************************)
 
-let local_assum (na, t) =
-  let open Context.Rel.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let open Context.Rel.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 module ExtraEnv =
 struct
 
@@ -94,7 +84,7 @@ let get_extra env =
   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
-    (Environ.rel_context env) ~init:(empty_csubst, [], avoid, named_context env)
+    (rel_context env) ~init:(empty_csubst, [], avoid, named_context env)
 
 let make_env env = { env = env; extra = lazy (get_extra env) }
 let rel_context env = rel_context env.env
@@ -116,7 +106,7 @@ let lookup_named id env = lookup_named id env.env
 let e_new_evar env evdref ?src ?naming typ =
   let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in
   let open Context.Named.Declaration in
-  let inst_vars = List.map (get_id %> EConstr.mkVar) (named_context env.env) in
+  let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in
   let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in
   let (subst, vsubst, _, nc) = Lazy.force env.extra in
   let typ' = subst2 subst vsubst typ in
@@ -128,7 +118,7 @@ let e_new_evar env evdref ?src ?naming typ =
   e
 
 let push_rec_types (lna,typarray,_) env =
-  let ctxt = Array.map2_i (fun i na t -> local_assum (na, lift i t)) lna typarray in
+  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
 
 end
@@ -434,7 +424,6 @@ let pretype_id pretype k0 loc env evdref lvar id =
   (* Look for the binder of [id] *)
   try
     let (n,_,typ) = lookup_rel_id id (rel_context env) in
-    let typ = EConstr.of_constr typ in
       { uj_val  = mkRel n; uj_type = lift n typ }
   with Not_found ->
     let env = ltac_interp_name_env k0 lvar env in
@@ -468,7 +457,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
       end;
       (* Check if [id] is a section or goal variable *)
       try
-	  { uj_val  = mkVar id; uj_type = EConstr.of_constr (NamedDecl.get_type (lookup_named id env)) }
+	  { uj_val  = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) }
       with Not_found ->
 	  (* [id] not found, standard error message *)
 	  error_var_not_found ~loc id
@@ -511,7 +500,7 @@ let pretype_ref loc evdref env ref us =
   match ref with
   | VarRef id ->
       (* Section variable *)
-      (try make_judge (mkVar id) (EConstr.of_constr (NamedDecl.get_type (lookup_named id env)))
+      (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id env))
        with Not_found ->
          (* This may happen if env is a goal env and section variables have
             been cleared - section variables should be different from goal
@@ -614,14 +603,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     [] -> ctxt
       | (na,bk,None,ty)::bl ->
         let ty' = pretype_type empty_valcon env evdref lvar ty in
-	let dcl = local_assum (na, ty'.utj_val) in
-        let dcl' = local_assum (ltac_interp_name lvar na,ty'.utj_val) 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
       | (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 = local_def (na, bd'.uj_val, ty'.utj_val) in
-        let dcl' = local_def (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) 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
     let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in
     let larj =
@@ -793,7 +782,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
-    let var = local_assum (name, j.utj_val) in
+    let var = LocalAssum (name, j.utj_val) in
     let j' = pretype rng (push_rel 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
@@ -809,7 +798,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         let j = pretype_type empty_valcon env evdref lvar c2 in
           { j with utj_val = lift 1 j.utj_val }
       | Name _ ->
-        let var = local_assum (name, j.utj_val) in
+        let var = LocalAssum (name, j.utj_val) in
         let env' = push_rel var env in
           pretype_type empty_valcon env' evdref lvar c2
     in
@@ -837,7 +826,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
-    let var = local_def (name, j.uj_val, t) in
+    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 name = ltac_interp_name lvar name in
@@ -861,6 +850,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       user_err ~loc:loc (str "Destructing let on this type expects " ++ 
 	int cs.cs_nargs ++ str " variables.");
     let fsign, record = 
+      let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in
       match get_projections env.ExtraEnv.env indf with
       | None ->
 	 List.map2 set_name (List.rev nal) cs.cs_args, false
@@ -870,7 +860,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  | na :: names, (LocalAssum (_,t) :: l) ->
             let t = EConstr.of_constr t in
 	    let proj = Projection.make ps.(cs.cs_nargs - k) true in
-	    local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t)
+	    LocalDef (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t)
 	    :: aux (n+1) (k + 1) names l
 	  | na :: names, (decl :: l) ->
 	    set_name na decl :: aux (n+1) k names l
@@ -896,6 +886,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	else arsgn
     in
       let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in
+      let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
       let nar = List.length arsgn in
 	  (match po with
 	  | Some p ->
@@ -903,6 +894,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    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 p = it_mkLambda_or_LetIn ccl psign in
 	    let inst =
 	      (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs)
@@ -956,6 +948,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       in
       let nar = List.length arsgn in
       let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in
+      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
@@ -978,17 +971,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let n = Context.Rel.length cs.cs_args in
 	let pi = lift n pred in (* liftn n 2 pred ? *)
 	let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
+        let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
 	let csgn =
 	  if not !allow_anonymous_refs then
-	    List.map (set_name Anonymous) cs.cs_args
+	    List.map (set_name Anonymous) cs_args
 	  else
 	    List.map (map_name (function Name _ as n -> n
 				       | Anonymous -> Name Namegen.default_non_dependent_ident))
-		     cs.cs_args
+		     cs_args
 	in
 	let env_c = push_rel_context csgn env in
 	let bj = pretype (mk_tycon pi) env_c evdref lvar b in
-	  it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
+	  it_mkLambda_or_LetIn bj.uj_val cs_args in
       let b1 = f cstrs.(0) b1 in
       let b2 = f cstrs.(1) b2 in
       let v =
@@ -1060,12 +1054,10 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
       with Not_found ->
       try
         let (n,_,t') = lookup_rel_id id (rel_context env) in
-        let t' = EConstr.of_constr t' in
         if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found
       with Not_found ->
       try
         let t' = env |> lookup_named id |> NamedDecl.get_type in
-        let t' = EConstr.of_constr t' in
         if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found
       with Not_found ->
         user_err ~loc  (str "Cannot interpret " ++
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index bc5c629f4..a1585ef52 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -13,9 +13,9 @@ open Term
 open Termops
 open Univ
 open Evd
+open Environ
 open EConstr
 open Vars
-open Environ
 open Context.Rel.Declaration
 
 exception Elimconst
@@ -609,14 +609,6 @@ let pr_state (tm,sk) =
   let pr c = Termops.print_constr c in
   h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk)
 
-let local_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 (*************************************)
 (*** Reduction Functions Operators ***)
 (*************************************)
@@ -851,12 +843,12 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     match c0 with
     | Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA ->
       (match lookup_rel n env with
-      | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n (EConstr.of_constr body), stack)
+      | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack)
       | _ -> fold ())
     | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
       (match lookup_named id env with
       | LocalDef (_,body,_) ->
-	whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (EConstr.of_constr body, stack)
+	whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack)
       | _ -> fold ())
     | Evar ev -> fold ()
     | Meta ev ->
@@ -958,7 +950,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
 	apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack
       | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
-	let env' = push_rel (local_assum (na, t)) env in
+	let env' = push_rel (LocalAssum (na, t)) env in
 	let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in
         (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with
         | App (f,cl) ->
@@ -1468,7 +1460,7 @@ let splay_prod env sigma =
     let t = whd_all env sigma c in
     match EConstr.kind sigma t with
       | Prod (n,a,c0) ->
-	  decrec (push_rel (local_assum (n,a)) env)
+	  decrec (push_rel (LocalAssum (n,a)) env)
 	    (bind_assum (n,a)::m) c0
       | _ -> m,t
   in
@@ -1479,7 +1471,7 @@ let splay_lam env sigma =
     let t = whd_all env sigma c in
     match EConstr.kind sigma t with
       | Lambda (n,a,c0) ->
-	  decrec (push_rel (local_assum (n,a)) env)
+	  decrec (push_rel (LocalAssum (n,a)) env)
 	    (bind_assum (n,a)::m) c0
       | _ -> m,t
   in
@@ -1490,11 +1482,11 @@ let splay_prod_assum env sigma =
     let t = whd_allnolet env sigma c in
     match EConstr.kind sigma t with
     | Prod (x,t,c)  ->
-	prodec_rec (push_rel (local_assum (x,t)) env)
-	  (Context.Rel.add (local_assum (x,t)) l) c
+	prodec_rec (push_rel (LocalAssum (x,t)) env)
+	  (Context.Rel.add (LocalAssum (x,t)) l) c
     | LetIn (x,b,t,c) ->
-	prodec_rec (push_rel (local_def (x,b,t)) env)
-	  (Context.Rel.add (local_def (x,b,t)) l) c
+	prodec_rec (push_rel (LocalDef (x,b,t)) env)
+	  (Context.Rel.add (LocalDef (x,b,t)) l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> 
       let t' = whd_all env sigma t in
@@ -1515,8 +1507,8 @@ let splay_prod_n env sigma n =
   let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
     match EConstr.kind sigma (whd_all env sigma c) with
       | Prod (n,a,c0) ->
-	  decrec (push_rel (local_assum (n,a)) env)
-	    (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
+	  decrec (push_rel (LocalAssum (n,a)) env)
+	    (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0
       | _                      -> invalid_arg "splay_prod_n"
   in
   decrec env n Context.Rel.empty
@@ -1525,8 +1517,8 @@ let splay_lam_n env sigma n =
   let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
     match EConstr.kind sigma (whd_all env sigma c) with
       | Lambda (n,a,c0) ->
-	  decrec (push_rel (local_assum (n,a)) env)
-	    (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
+	  decrec (push_rel (LocalAssum (n,a)) env)
+	    (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0
       | _                      -> invalid_arg "splay_lam_n"
   in
   decrec env n Context.Rel.empty
@@ -1566,8 +1558,8 @@ let find_conclusion env sigma =
   let rec decrec env c =
     let t = whd_all env sigma c in
     match EConstr.kind sigma t with
-      | Prod (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
-      | Lambda (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
+      | Prod (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0
+      | Lambda (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0
       | t -> t
   in
   decrec env
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index dcc11cfcf..15ddeb15c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -217,10 +217,10 @@ val splay_prod : env ->  evar_map -> constr -> (Name.t * constr) list * constr
 val splay_lam : env ->  evar_map -> constr -> (Name.t * constr) list * constr
 val splay_arity : env ->  evar_map -> constr -> (Name.t * constr) list * sorts
 val sort_of_arity : env -> evar_map -> constr -> sorts
-val splay_prod_n : env ->  evar_map -> int -> constr -> Context.Rel.t * constr
-val splay_lam_n : env ->  evar_map -> int -> constr -> Context.Rel.t * constr
+val splay_prod_n : env ->  evar_map -> int -> constr -> rel_context * constr
+val splay_lam_n : env ->  evar_map -> int -> constr -> rel_context * constr
 val splay_prod_assum :
-  env ->  evar_map -> constr -> Context.Rel.t * constr
+  env ->  evar_map -> constr -> rel_context * constr
 
 type 'a miota_args = {
   mP      : constr;     (** the result type *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a9529d560..bb1b2901e 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -50,14 +50,6 @@ let anomaly_on_error f x =
  try f x
  with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e)
 
-let local_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 let get_type_from_constraints env sigma t =
   if isEvar sigma (fst (decompose_app_vect sigma t)) then
     match
@@ -84,13 +76,13 @@ let rec subst_type env sigma typ = function
 let sort_of_atomic_type env sigma ft args =
   let rec concl_of_arity env n ar args =
     match EConstr.kind sigma (whd_all env sigma ar), args with
-    | Prod (na, t, b), h::l -> concl_of_arity (push_rel (local_def (na, lift n h, t)) env) (n + 1) b l
+    | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l
     | Sort s, [] -> s
     | _ -> retype_error NotASort
   in concl_of_arity env 0 ft (Array.to_list args)
 
 let type_of_var env id =
-  try EConstr.of_constr (NamedDecl.get_type (lookup_named id env))
+  try NamedDecl.get_type (lookup_named id env)
   with Not_found -> retype_error (BadVariable id)
 
 let decomp_sort env sigma t =
@@ -105,7 +97,7 @@ let retype ?(polyprop=true) sigma =
       (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus)
        with Not_found -> retype_error (BadMeta n))
     | Rel n ->
-	let ty = EConstr.of_constr (RelDecl.get_type (lookup_rel n env)) in
+	let ty = RelDecl.get_type (lookup_rel n env) in
         lift n ty
     | Var id -> type_of_var env id
     | Const cst -> EConstr.of_constr (rename_type_of_constant env cst)
@@ -128,9 +120,9 @@ let retype ?(polyprop=true) sigma =
           | Prod _ -> whd_beta sigma (applist (t, [c]))
           | _ -> t)
     | Lambda (name,c1,c2) ->
-          mkProd (name, c1, type_of (push_rel (local_assum (name,c1)) env) c2)
+          mkProd (name, c1, type_of (push_rel (LocalAssum (name,c1)) env) c2)
     | LetIn (name,b,c1,c2) ->
-         subst1 b (type_of (push_rel (local_def (name,b,c1)) env) c2)
+         subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2)
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
     | App(f,args) when is_template_polymorphic env sigma f ->
@@ -153,7 +145,7 @@ let retype ?(polyprop=true) sigma =
     | Sort (Prop c) -> type1_sort
     | Sort (Type u) -> Type (Univ.super u)
     | Prod (name,t,c2) ->
-        (match (sort_of env t, sort_of (push_rel (local_assum (name,t)) env) c2) with
+        (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with
 	  | _, (Prop Null as s) -> s
           | Prop _, (Prop Pos as s) -> s
           | Type _, (Prop Pos as s) when is_impredicative_set env -> s
@@ -174,7 +166,7 @@ let retype ?(polyprop=true) sigma =
     | Sort (Prop c) -> InType
     | Sort (Type u) -> InType
     | Prod (name,t,c2) ->
-	let s2 = sort_family_of (push_rel (local_assum (name,t)) env) c2 in
+	let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
 	if not (is_impredicative_set env) &&
 	   s2 == InSet && sort_family_of env t == InType then InType else s2
     | App(f,args) when is_template_polymorphic env sigma f ->
@@ -249,7 +241,7 @@ let sorts_of_context env evc ctxt =
   | [] -> env,[]
   | d :: ctxt ->
       let env,sorts = aux ctxt in
-      let s = get_sort_of env evc (EConstr.of_constr (RelDecl.get_type d)) in
+      let s = get_sort_of env evc (RelDecl.get_type d) in
       (push_rel d env,s::sorts) in
   snd (aux ctxt)
 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index ce9e1635f..25129db1c 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -44,7 +44,7 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
 val type_of_global_reference_knowing_conclusion :
   env -> evar_map -> constr -> types -> evar_map * types
 
-val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list
+val sorts_of_context : env -> evar_map -> rel_context -> sorts list
 
 val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 4abfc26fc..9f3f3c7e5 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -14,11 +14,11 @@ open Term
 open Libnames
 open Globnames
 open Termops
+open Environ
 open EConstr
 open Vars
 open Find_subterm
 open Namegen
-open Environ
 open CClosure
 open Reductionops
 open Cbv
@@ -60,7 +60,7 @@ let is_evaluable env = function
 let value_of_evaluable_ref env evref u =
   match evref with
   | EvalConstRef con -> 
-    (try constant_value_in env (con,u)
+    EConstr.of_constr (try constant_value_in env (con,u)
     with NotEvaluableConst IsProj -> 
       raise (Invalid_argument "value_of_evaluable_ref"))
   | EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get
@@ -115,9 +115,9 @@ let unsafe_reference_opt_value env sigma eval =
     | Declarations.Def c -> Some (EConstr.of_constr (Mod_subst.force_constr c))
     | _ -> None)
   | EvalVar id ->
-      env |> lookup_named id |> NamedDecl.get_value |> Option.map EConstr.of_constr
+      env |> lookup_named id |> NamedDecl.get_value
   | EvalRel n ->
-      env |> lookup_rel n |> RelDecl.get_value |> Option.map (EConstr.of_constr %> lift n)
+      env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n)
   | EvalEvar ev ->
     match EConstr.kind sigma (mkEvar ev) with
     | Evar _ -> None
@@ -127,9 +127,9 @@ let reference_opt_value env sigma eval u =
   match eval with
   | EvalConst cst -> Option.map EConstr.of_constr (constant_opt_value_in env (cst,u))
   | EvalVar id ->
-      env |> lookup_named id |> NamedDecl.get_value |> Option.map EConstr.of_constr
+      env |> lookup_named id |> NamedDecl.get_value
   | EvalRel n ->
-      env |> lookup_rel n |> RelDecl.get_value |> Option.map (EConstr.of_constr %> lift n)
+      env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n)
   | EvalEvar ev ->
     match EConstr.kind sigma (mkEvar ev) with
     | Evar _ -> None
@@ -146,11 +146,11 @@ let reference_value env sigma c u =
 (* One reuses the name of the function after reduction of the fixpoint  *)
 
 type constant_evaluation =
-  | EliminationFix of int * int * (int * (int * EConstr.t) list * int)
+  | EliminationFix of int * int * (int * (int * constr) list * int)
   | EliminationMutualFix of
       int * evaluable_reference *
       ((int*evaluable_reference) option array *
-       (int * (int * EConstr.t) list * int))
+       (int * (int * constr) list * int))
   | EliminationCases of int
   | EliminationProj of int
   | NotAnElimination
@@ -261,22 +261,13 @@ let invert_name labs l na0 env sigma ref = function
    [compute_consteval_mutual_fix] only one by one, until finding the
    last one before the Fix if the latter is mutually defined *)
 
-let local_assum (na, t) =
-  let open Context.Rel.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let open Context.Rel.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 let compute_consteval_direct env sigma ref =
   let rec srec env n labs onlyproj c =
     let c',l = whd_betadeltazeta_stack env sigma c in
     match EConstr.kind sigma c' with
       | Lambda (id,t,g) when List.is_empty l && not onlyproj ->
-	  srec (push_rel (local_assum (id,t)) env) (n+1) (t::labs) onlyproj g
+          let open Context.Rel.Declaration in
+	  srec (push_rel (LocalAssum (id,t)) env) (n+1) (t::labs) onlyproj g
       | Fix fix when not onlyproj ->
 	  (try check_fix_reversibility sigma labs l fix
 	  with Elimconst -> NotAnElimination)
@@ -295,7 +286,8 @@ let compute_consteval_mutual_fix env sigma ref =
     let nargs = List.length l in
     match EConstr.kind sigma c' with
       | Lambda (na,t,g) when List.is_empty l ->
-	  srec (push_rel (local_assum (na,t)) env) (minarg+1) (t::labs) ref g
+          let open Context.Rel.Declaration in
+	  srec (push_rel (LocalAssum (na,t)) env) (minarg+1) (t::labs) ref g
       | Fix ((lv,i),(names,_,_)) ->
 	  (* Last known constant wrapping Fix is ref = [labs](Fix l) *)
 	  (match compute_consteval_direct env sigma ref with
@@ -386,7 +378,7 @@ let make_elim_fun (names,(nbfix,lv,n)) u largs =
 (* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]:
    do so that the reduction uses this extra information *)
 
-let dummy = Constr.mkProp
+let dummy = mkProp
 let vfx = Id.of_string "_expanded_fix_"
 let vfun = Id.of_string "_eliminator_function_"
 let venv = let open Context.Named.Declaration in
@@ -405,7 +397,7 @@ let substl_with_function subst sigma constr =
       match v.(i-k-1) with
       | (fx, Some (min, ref)) ->
         let sigma = Sigma.Unsafe.of_evar_map !evd in
-        let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma (EConstr.of_constr dummy) in
+        let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma dummy in
         let sigma = Sigma.to_evar_map sigma in
         evd := sigma;
         minargs := Evar.Map.add evk min !minargs;
@@ -466,7 +458,7 @@ let substl_checking_arity env subst sigma c =
   in
   nf_fix body
 
-type fix_reduction_result = NotReducible | Reduced of (EConstr.t * EConstr.t list)
+type fix_reduction_result = NotReducible | Reduced of (constr * constr list)
 
 let reduce_fix whdfun sigma fix stack =
   match fix_recarg fix (Stack.append_app_list stack Stack.empty) with
@@ -557,9 +549,9 @@ let match_eval_ref_value env sigma constr =
   | Const (sp, u) when is_evaluable env (EvalConstRef sp) ->
     Some (EConstr.of_constr (constant_value_in env (sp, u)))
   | Var id when is_evaluable env (EvalVarRef id) -> 
-     env |> lookup_named id |> NamedDecl.get_value |> Option.map EConstr.of_constr
+     env |> lookup_named id |> NamedDecl.get_value
   | Rel n ->
-     env |> lookup_rel n |> RelDecl.get_value |> Option.map (EConstr.of_constr %> lift n)
+     env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n)
   | _ -> None
 
 let special_red_case env sigma whfun (ci, p, c, lf) =
@@ -625,12 +617,12 @@ let whd_nothing_for_iota env sigma s =
       | Rel n ->
           let open Context.Rel.Declaration in
 	  (match lookup_rel n env with
-	     | LocalDef (_,body,_) -> whrec (lift n (EConstr.of_constr body), stack)
+	     | LocalDef (_,body,_) -> whrec (lift n body, stack)
 	     | _ -> s)
       | Var id ->
           let open Context.Named.Declaration in
 	  (match lookup_named id env with
-	     | LocalDef (_,body,_) -> whrec (EConstr.of_constr body, stack)
+	     | LocalDef (_,body,_) -> whrec (body, stack)
 	     | _ -> s)
       | Evar ev -> s
       | Meta ev ->
@@ -834,7 +826,8 @@ let try_red_product env sigma c =
              | _ -> simpfun (mkApp (redrec env f, l)))
       | Cast (c,_,_) -> redrec env c
       | Prod (x,a,b) ->
-	  mkProd (x, a, redrec (push_rel (local_assum (x, a)) env) b)
+          let open Context.Rel.Declaration in
+	  mkProd (x, a, redrec (push_rel (LocalAssum (x, a)) env) b)
       | LetIn (x,a,b,t) -> redrec env (Vars.subst1 a t)
       | Case (ci,p,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf))
       | Proj (p, c) -> 
@@ -1053,7 +1046,7 @@ let substlin env sigma evalref n (nowhere_except_in,locs) c =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref n in
   assert (List.for_all (fun x -> x >= 0) locs);
-  let value u = EConstr.of_constr (value_of_evaluable_ref env evalref u) in
+  let value u = value_of_evaluable_ref env evalref u in
   let rec substrec () c =
     if nowhere_except_in && !pos > maxocc then c
     else 
@@ -1192,7 +1185,7 @@ let reduce_to_ind_gen allow_product env sigma t =
       | Prod (n,ty,t') ->
 	  let open Context.Rel.Declaration in
 	  if allow_product then
-	    elimrec (push_rel (local_assum (n,ty)) env) t' ((local_assum (n,ty))::l)
+	    elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l)
 	  else
 	    user_err  (str"Not an inductive definition.")
       | _ ->
@@ -1270,7 +1263,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
       | Prod (n,ty,t') ->
           if allow_product then
 	    let open Context.Rel.Declaration in
-	    elimrec (push_rel (local_assum (n,t)) env) t' ((local_assum (n,ty))::l)
+	    elimrec (push_rel (LocalAssum (n,t)) env) t' ((LocalAssum (n,ty))::l)
           else
             error_cannot_recognize ref
       | _ ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 50ae66eb0..ce570ee12 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -300,6 +300,7 @@ let build_subclasses ~check env sigma glob pri =
 	   | Some (Backward, _) -> None
 	   | Some (Forward, pri') ->
 	     let proj = Option.get proj in
+	     let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in
 	     let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
 	       if check && check_instance env sigma (EConstr.of_constr body) then None
 	       else 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index e95aba695..0c30296d3 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -67,7 +67,7 @@ val dest_class_app : env -> evar_map -> EConstr.constr -> typeclass puniverses *
 val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses
 
 (** Just return None if not a class *)
-val class_of_constr : evar_map -> EConstr.constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option
+val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * (typeclass puniverses * constr list)) option
   
 val instance_impl : instance -> global_reference
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e6f1e46b6..bdd3663d1 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -12,9 +12,9 @@ open Pp
 open CErrors
 open Util
 open Term
+open Environ
 open EConstr
 open Vars
-open Environ
 open Reductionops
 open Inductive
 open Inductiveops
@@ -23,14 +23,6 @@ open Arguments_renaming
 open Pretype_errors
 open Context.Rel.Declaration
 
-let local_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 let push_rec_types pfix env =
   let (i, c, t) = pfix in
   let inj c = EConstr.Unsafe.to_constr c in
@@ -101,14 +93,15 @@ let max_sort l =
 
 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 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 =
     let pt' = whd_all env !evdref pt in
     match EConstr.kind !evdref pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
-        if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error ();
-        srec (push_rel (local_assum (na1,a1)) env) t ar'
+        if not (Evarconv.e_cumul env evdref a1 a1') then error ();
+        srec (push_rel (LocalAssum (na1,a1)) env) t ar'
     | Sort s, [] ->
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
         then error ()
@@ -326,14 +319,14 @@ let rec execute env evdref cstr =
     | Lambda (name,c1,c2) ->
         let j = execute env evdref c1 in
 	let var = e_type_judgment env evdref j in
-	let env1 = push_rel (local_assum (name, var.utj_val)) env in
+	let env1 = push_rel (LocalAssum (name, var.utj_val)) env in
         let j' = execute env1 evdref c2 in
         judge_of_abstraction env1 name var j'
 
     | Prod (name,c1,c2) ->
         let j = execute env evdref c1 in
         let varj = e_type_judgment env evdref j in
-	let env1 = push_rel (local_assum (name, varj.utj_val)) env in
+	let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in
         let j' = execute env1 evdref c2 in
         let varj' = e_type_judgment env1 evdref j' in
 	judge_of_product env name varj varj'
@@ -343,7 +336,7 @@ let rec execute env evdref cstr =
         let j2 = execute env evdref c2 in
         let j2 = e_type_judgment env evdref j2 in
         let _ =  e_judge_of_cast env evdref j1 DEFAULTcast j2 in
-        let env1 = push_rel (local_def (name, j1.uj_val, j2.utj_val)) env in
+        let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in
         let j3 = execute env1 evdref c3 in
         judge_of_letin env name j1 j2 j3
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 04cc4253e..0d6dcffc1 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -14,10 +14,10 @@ open Util
 open Names
 open Term
 open Termops
+open Environ
 open EConstr
 open Vars
 open Namegen
-open Environ
 open Evd
 open Reduction
 open Reductionops
@@ -91,7 +91,6 @@ let abstract_scheme env evd c l lname_typ =
     (fun (t,evd) (locc,a) decl ->
        let na = RelDecl.get_name decl in
        let ta = RelDecl.get_type decl in
-       let ta = EConstr.of_constr ta in
        let na = match EConstr.kind evd a with Var id -> Name id | _ -> na in
 (* [occur_meta ta] test removed for support of eelim/ecase but consequences
    are unclear...
@@ -1627,6 +1626,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
   let likefirst = clause_with_generic_occurrences occs in
   let mkvarid () = EConstr.mkVar id in
   let compute_dependency _ d (sign,depdecls) =
+    let d = map_named_decl EConstr.of_constr d in
     let hyp = NamedDecl.get_id d in
     match occurrences_of_hyp hyp occs with
     | NoOccurrences, InHyp ->
@@ -1634,7 +1634,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     | AllOccurrences, InHyp as occ ->
         let occ = if likefirst then LikeFirst else AtOccs occ in
         let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in
-        if Context.Named.Declaration.equal Constr.equal d newdecl
+        if Context.Named.Declaration.equal (EConstr.eq_constr sigma) d newdecl
            && not (indirectly_dependent sigma c d depdecls)
         then
           if check_occs && not (in_every_hyp occs)
@@ -1688,7 +1688,7 @@ type abstraction_request =
 
 type 'r abstraction_result =
   Names.Id.t * named_context_val *
-    Context.Named.Declaration.t list * Names.Id.t option *
+    named_declaration list * Names.Id.t option *
     types * (constr, 'r) Sigma.sigma option
 
 let make_abstraction env evd ccl abs =
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 41dcb8ed3..6760283d2 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -82,7 +82,7 @@ val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
 
 type 'r abstraction_result =
   Names.Id.t * named_context_val *
-    Context.Named.Declaration.t list * Names.Id.t option *
+    named_declaration list * Names.Id.t option *
     types * (constr, 'r) Sigma.sigma option
 
 val make_abstraction : env -> 'r Sigma.t -> constr ->