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.

8 files changed, 252 insertions, 178 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 629be8e4b..657285de2 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -77,6 +77,10 @@ type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
 type unsafe_type_judgment = types Environ.punsafe_type_judgment
+type named_declaration = (constr, types) Context.Named.Declaration.pt
+type rel_declaration = (constr, types) Context.Rel.Declaration.pt
+type named_context = (constr, types) Context.Named.pt
+type rel_context = (constr, types) Context.Rel.pt
 
 let in_punivs a = (a, Univ.Instance.empty)
 
@@ -201,14 +205,6 @@ let decompose_app sigma c =
     | App (f,cl) -> (f, Array.to_list cl)
     | _ -> (c,[])
 
-let local_assum (na, t) =
-  let open Rel.Declaration in
-  LocalAssum (na, unsafe_to_constr t)
-
-let local_def (na, b, t) =
-  let open Rel.Declaration in
-  LocalDef (na, unsafe_to_constr b, unsafe_to_constr t)
-
 let decompose_lam sigma c =
   let rec lamdec_rec l c = match kind sigma c with
     | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
@@ -218,38 +214,41 @@ let decompose_lam sigma c =
   lamdec_rec [] c
 
 let decompose_lam_assum sigma c =
+  let open Rel.Declaration in
   let rec lamdec_rec l c =
     match kind sigma c with
-    | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) c
-    | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) c
+    | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) c
+    | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c
     | Cast (c,_,_)      -> lamdec_rec l c
     | _               -> l,c
   in
   lamdec_rec Context.Rel.empty c
 
 let decompose_lam_n_assum sigma n c =
+  let open Rel.Declaration in
   if n < 0 then
     error "decompose_lam_n_assum: integer parameter must be positive";
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else
       match kind sigma c with
-      | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c
-      | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) n c
+      | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
+      | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c
       | Cast (c,_,_)      -> lamdec_rec l n c
       | c -> error "decompose_lam_n_assum: not enough abstractions"
   in
   lamdec_rec Context.Rel.empty n c
 
 let decompose_lam_n_decls sigma n =
+  let open Rel.Declaration in
   if n < 0 then
     error "decompose_lam_n_decls: integer parameter must be positive";
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else
       match kind sigma c with
-      | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c
-      | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) (n-1) c
+      | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
+      | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
       | Cast (c,_,_)      -> lamdec_rec l n c
       | c -> error "decompose_lam_n_decls: not enough abstractions"
   in
@@ -264,24 +263,26 @@ let decompose_prod sigma c =
   proddec_rec [] c
 
 let decompose_prod_assum sigma c =
+  let open Rel.Declaration in
   let rec proddec_rec l c =
     match kind sigma c with
-    | Prod (x,t,c)  -> proddec_rec (Context.Rel.add (local_assum (x,t)) l) c
-    | LetIn (x,b,t,c) -> proddec_rec (Context.Rel.add (local_def (x,b,t)) l) c
+    | Prod (x,t,c)  -> proddec_rec (Context.Rel.add (LocalAssum (x,t)) l) c
+    | LetIn (x,b,t,c) -> proddec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c
     | Cast (c,_,_)      -> proddec_rec l c
     | _               -> l,c
   in
   proddec_rec Context.Rel.empty c
 
 let decompose_prod_n_assum sigma n c =
+  let open Rel.Declaration in
   if n < 0 then
     error "decompose_prod_n_assum: integer parameter must be positive";
   let rec prodec_rec l n c =
     if Int.equal n 0 then l,c
     else
       match kind sigma c with
-      | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c
-      | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (local_def (x,b,t)) l) (n-1) c
+      | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
+      | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
       | Cast (c,_,_)      -> prodec_rec l n c
       | c -> error "decompose_prod_n_assum: not enough assumptions"
   in
@@ -413,24 +414,26 @@ let iter sigma f c = match kind sigma c with
   | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
   | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
 
-let iter_with_full_binders sigma g f n c = match kind sigma c with
+let iter_with_full_binders sigma g f n c =
+  let open Context.Rel.Declaration in
+  match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> ()
   | Cast (c,_,t) -> f n c; f n t
-  | Prod (na,t,c) -> f n t; f (g (local_assum (na, t)) n) c
-  | Lambda (na,t,c) -> f n t; f (g (local_assum (na, t)) n) c
-  | LetIn (na,b,t,c) -> f n b; f n t; f (g (local_def (na, b, t)) n) c
+  | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
+  | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
+  | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
   | App (c,l) -> f n c; CArray.Fun1.iter f n l
   | Evar (_,l) -> CArray.Fun1.iter f n l
   | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
-    let n' = Array.fold_left2 (fun n na t -> g (local_assum (na,t)) n) n lna tl in
+    let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in
     Array.iter (f n') bl
   | CoFix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
-    let n' = Array.fold_left2 (fun n na t -> g (local_assum (na,t)) n) n lna tl in
+    let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in
     Array.iter (f n') bl
 
 let iter_with_binders sigma g f n c =
@@ -611,14 +614,14 @@ let rec isArity sigma c =
 let mkProd_or_LetIn decl c =
   let open Context.Rel.Declaration in
   match decl with
-  | LocalAssum (na,t) -> mkProd (na, of_constr t, c)
-  | LocalDef (na,b,t) -> mkLetIn (na, of_constr b, of_constr t, c)
+  | LocalAssum (na,t) -> mkProd (na, t, c)
+  | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
 
 let mkLambda_or_LetIn decl c =
   let open Context.Rel.Declaration in
   match decl with
-  | LocalAssum (na,t) -> mkLambda (na, of_constr t, c)
-  | LocalDef (na,b,t) -> mkLetIn (na, of_constr b, of_constr t, c)
+  | LocalAssum (na,t) -> mkLambda (na, t, c)
+  | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
 
 let mkNamedProd id typ c = mkProd (Name id, typ, Vars.subst_var id c)
 let mkNamedLambda id typ c = mkLambda (Name id, typ, Vars.subst_var id c)
@@ -627,18 +630,56 @@ let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, Vars.subst_var id c2)
 let mkNamedProd_or_LetIn decl c =
   let open Context.Named.Declaration in
   match decl with
-    | LocalAssum (id,t) -> mkNamedProd id (of_constr t) c
-    | LocalDef (id,b,t) -> mkNamedLetIn id (of_constr b) (of_constr t) c
+    | LocalAssum (id,t) -> mkNamedProd id t c
+    | LocalDef (id,b,t) -> mkNamedLetIn id b t c
 
 let mkNamedLambda_or_LetIn decl c =
   let open Context.Named.Declaration in
   match decl with
-    | LocalAssum (id,t) -> mkNamedLambda id (of_constr t) c
-    | LocalDef (id,b,t) -> mkNamedLetIn id (of_constr b) (of_constr t) c
+    | LocalAssum (id,t) -> mkNamedLambda id t c
+    | LocalDef (id,b,t) -> mkNamedLetIn id b t c
 
 let it_mkProd_or_LetIn t ctx = List.fold_left (fun c d -> mkProd_or_LetIn d c) t ctx
 let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d c) t ctx
 
+open Context
+open Environ
+
+let sym : type a b. (a, b) eq -> (b, a) eq = fun Refl -> Refl
+
+let cast_rel_decl :
+  type a b. (a,b) eq -> (a, a) Rel.Declaration.pt -> (b, b) Rel.Declaration.pt =
+  fun Refl x -> x
+
+let cast_rel_context :
+  type a b. (a,b) eq -> (a, a) Rel.pt -> (b, b) Rel.pt =
+  fun Refl x -> x
+
+let cast_named_decl :
+  type a b. (a,b) eq -> (a, a) Named.Declaration.pt -> (b, b) Named.Declaration.pt =
+  fun Refl x -> x
+
+let cast_named_context :
+  type a b. (a,b) eq -> (a, a) Named.pt -> (b, b) Named.pt =
+  fun Refl x -> x
+
+let push_rel d e = push_rel (cast_rel_decl unsafe_eq d) e
+let push_rel_context d e = push_rel_context (cast_rel_context unsafe_eq d) e
+let push_named d e = push_named (cast_named_decl unsafe_eq d) e
+let push_named_context d e = push_named_context (cast_named_context unsafe_eq d) e
+let push_named_context_val d e = push_named_context_val (cast_named_decl unsafe_eq d) e
+
+let rel_context e = cast_rel_context (sym unsafe_eq) (rel_context e)
+let named_context e = cast_named_context (sym unsafe_eq) (named_context e)
+
+let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq e)
+let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e)
+
+let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
+let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
+let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
+
+
 module Unsafe =
 struct
 let to_constr = unsafe_to_constr
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index cb671154c..d6b2113d2 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -10,6 +10,7 @@ open CSig
 open Names
 open Constr
 open Context
+open Environ
 
 type t
 (** Type of incomplete terms. Essentially a wrapper around {!Constr.t} ensuring
@@ -22,6 +23,10 @@ type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
 type unsafe_type_judgment = types Environ.punsafe_type_judgment
+type named_declaration = (constr, types) Context.Named.Declaration.pt
+type rel_declaration = (constr, types) Context.Rel.Declaration.pt
+type named_context = (constr, types) Context.Named.pt
+type rel_context = (constr, types) Context.Rel.pt
 
 (** {5 Destructors} *)
 
@@ -77,16 +82,16 @@ val mkArrow : t -> t -> t
 
 val applist : t * t list -> t
 
-val mkProd_or_LetIn : Rel.Declaration.t -> t -> t
-val mkLambda_or_LetIn : Rel.Declaration.t -> t -> t
-val it_mkProd_or_LetIn : t -> Rel.t -> t
-val it_mkLambda_or_LetIn : t -> Rel.t -> t
+val mkProd_or_LetIn : rel_declaration -> t -> t
+val mkLambda_or_LetIn : rel_declaration -> t -> t
+val it_mkProd_or_LetIn : t -> rel_context -> t
+val it_mkLambda_or_LetIn : t -> rel_context -> t
 
 val mkNamedLambda : Id.t -> types -> constr -> constr
 val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
 val mkNamedProd : Id.t -> types -> types -> types
-val mkNamedLambda_or_LetIn : Named.Declaration.t -> types -> types
-val mkNamedProd_or_LetIn : Named.Declaration.t -> types -> types
+val mkNamedLambda_or_LetIn : named_declaration -> types -> types
+val mkNamedProd_or_LetIn : named_declaration -> types -> types
 
 (** {6 Simple case analysis} *)
 
@@ -131,13 +136,13 @@ val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
 val decompose_app : Evd.evar_map -> t -> t * t list
 
 val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t
-val decompose_lam_assum : Evd.evar_map -> t -> Context.Rel.t * t
-val decompose_lam_n_assum : Evd.evar_map -> int -> t -> Context.Rel.t * t
-val decompose_lam_n_decls : Evd.evar_map -> int -> t -> Context.Rel.t * t
+val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t
+val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t
+val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t
 
 val decompose_prod : Evd.evar_map -> t -> (Name.t * t) list * t
-val decompose_prod_assum : Evd.evar_map -> t -> Context.Rel.t * t
-val decompose_prod_n_assum : Evd.evar_map -> int -> t -> Context.Rel.t * t
+val decompose_prod_assum : Evd.evar_map -> t -> rel_context * t
+val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t
 
 val existential_type : Evd.evar_map -> existential -> types
 
@@ -156,7 +161,7 @@ val map : Evd.evar_map -> (t -> t) -> t -> t
 val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
 val iter : Evd.evar_map -> (t -> unit) -> t -> unit
 val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
-val iter_with_full_binders : Evd.evar_map -> (Rel.Declaration.t -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
+val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
 val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
 (** {6 Substitutions} *)
@@ -184,6 +189,25 @@ val subst_univs_level_constr : Univ.universe_level_subst -> t -> t
 
 end
 
+(** {5 Environment handling} *)
+
+val push_rel : rel_declaration -> env -> env
+val push_rel_context : rel_context -> env -> env
+
+val push_named : named_declaration -> env -> env
+val push_named_context : named_context -> env -> env
+val push_named_context_val  : named_declaration -> named_context_val -> named_context_val
+
+val rel_context : env -> rel_context
+val named_context : env -> named_context
+
+val val_of_named_context : named_context -> named_context_val
+val named_context_of_val : named_context_val -> named_context
+
+val lookup_rel : int -> env -> rel_declaration
+val lookup_named : variable -> env -> named_declaration
+val lookup_named_val : variable -> named_context_val -> named_declaration
+
 (** {5 Unsafe operations} *)
 
 module Unsafe :
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 42620c0b5..0582e34be 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -139,12 +139,12 @@ let nf_named_context_evar sigma ctx =
   Context.Named.map (nf_evar0 sigma) ctx
 
 let nf_rel_context_evar sigma ctx =
-  Context.Rel.map (nf_evar0 sigma) ctx
+  Context.Rel.map (nf_evar sigma) ctx
 
 let nf_env_evar sigma env =
   let nc' = nf_named_context_evar sigma (Environ.named_context env) in
-  let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in
-    push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
+  let rel' = nf_rel_context_evar sigma (EConstr.rel_context env) in
+    EConstr.push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
 
 let nf_evar_info evc info = map_evar_info (nf_evar0 evc) info
 
@@ -320,7 +320,7 @@ let empty_csubst = (0, Int.Map.empty)
 
 type ext_named_context =
   csubst * (Id.t * EConstr.constr) list *
-  Id.Set.t * Context.Named.t
+  Id.Set.t * EConstr.named_context
 
 let push_var id (n, s) =
   let s = Int.Map.add n (EConstr.mkVar id) s in
@@ -330,7 +330,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
   let open EConstr in
   let open Vars in
   let map_decl f d =
-    NamedDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (f (EConstr.of_constr c))) d
+    NamedDecl.map_constr f d
   in
   let replace_var_named_declaration id0 id decl =
     let id' = NamedDecl.get_id decl in
@@ -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 (RelDecl.get_type decl) na) avoid
+      next_ident_away (id_of_name_using_hdchar empty_env (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) na) avoid
   in
   match extract_if_neq id na with
   | Some id0 when not (is_section_variable id0) ->
@@ -542,6 +542,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
 	       removed *)
 	    let evi = Evd.find_undefined !evdref evk in
 	    let ctxt = Evd.evar_filtered_context evi in
+	    let ctxt = List.map (fun d -> map_named_decl EConstr.of_constr d) ctxt in
 	    let (rids,filter) =
               List.fold_right2
                 (fun h a (ri,filter) ->
@@ -595,6 +596,7 @@ let clear_hyps_in_evi_main env evdref hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
      the contexts of the evars occurring in evi *)
+  let terms = List.map EConstr.Unsafe.to_constr terms in
   let global = Id.Set.exists is_section_variable ids in
   let terms =
     List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids global) terms in
@@ -616,10 +618,9 @@ let clear_hyps_in_evi_main env evdref hyps terms ids =
     in
       remove_hyps ids check_context check_value hyps
   in
-  (nhyps,terms)
+  (nhyps,List.map EConstr.of_constr terms)
 
 let clear_hyps_in_evi env evdref hyps concl ids =
-  let concl = EConstr.Unsafe.to_constr concl in
   match clear_hyps_in_evi_main env evdref hyps [concl] ids with
   | (nhyps,[nconcl]) -> (nhyps,nconcl)
   | _ -> assert false
@@ -746,6 +747,7 @@ let occur_evar_upto sigma n c =
    any type has type Type. May cause some trouble, but not so far... *)
 
 let judge_of_new_Type evd =
+  let open EConstr in
   let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in
   Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p)
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 67de18abc..2da4f8043 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -10,6 +10,7 @@ open Names
 open Term
 open Evd
 open Environ
+open EConstr
 
 (** This module provides useful higher-level functions for evar manipulation. *)
 
@@ -17,51 +18,51 @@ open Environ
 
 (** [new_meta] is a generator of unique meta variables *)
 val new_meta : unit -> metavariable
-val mk_new_meta : unit -> EConstr.constr
+val mk_new_meta : unit -> constr
 
 (** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
   env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?candidates:EConstr.constr list -> ?store:Store.t ->
+  ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> EConstr.types -> (EConstr.constr, 'r) Sigma.sigma
+  ?principal:bool -> types -> (constr, 'r) Sigma.sigma
 
 val new_pure_evar :
   named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?candidates:EConstr.constr list -> ?store:Store.t ->
+  ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> EConstr.types -> (evar, 'r) Sigma.sigma
+  ?principal:bool -> types -> (evar, 'r) Sigma.sigma
 
 val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma
 
 (** the same with side-effects *)
 val e_new_evar :
   env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?candidates:EConstr.constr list -> ?store:Store.t ->
+  ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> EConstr.types -> EConstr.constr
+  ?principal:bool -> types -> constr
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
   env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
-  (EConstr.constr * sorts, 'r) Sigma.sigma
+  (constr * sorts, 'r) Sigma.sigma
 
 val e_new_type_evar : env -> evar_map ref ->
   ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> EConstr.constr * sorts
+  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
 
-val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (EConstr.constr, 'r) Sigma.sigma
-val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> EConstr.constr
+val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
+val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
 
 val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
-  EConstr.constr list option -> (existential_key, 'r) Sigma.sigma
+  constr list option -> (existential_key, 'r) Sigma.sigma
 
 (** Polymorphic constants *)
 
-val new_global : 'r Sigma.t -> Globnames.global_reference -> (EConstr.constr, 'r) Sigma.sigma
-val e_new_global : evar_map ref -> Globnames.global_reference -> EConstr.constr
+val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma
+val e_new_global : evar_map ref -> Globnames.global_reference -> constr
 
 (** Create a fresh evar in a context different from its definition context:
    [new_evar_instance sign evd ty inst] creates a new evar of context
@@ -70,15 +71,15 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> EConstr.constr
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> 'r Sigma.t -> EConstr.types -> 
-  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:EConstr.constr list ->
+ named_context_val -> 'r Sigma.t -> types -> 
+  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
   ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool ->
-  EConstr.constr list -> (EConstr.constr, 'r) Sigma.sigma
+  constr list -> (constr, 'r) Sigma.sigma
 
 val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list
 
-val safe_evar_value : evar_map -> existential -> constr option
+val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
 
 (** {6 Evars/Metas switching...} *)
 
@@ -88,15 +89,15 @@ val non_instantiated : evar_map -> evar_info Evar.Map.t
 
 (** [head_evar c] returns the head evar of [c] if any *)
 exception NoHeadEvar
-val head_evar : evar_map -> EConstr.constr -> existential_key (** may raise NoHeadEvar *)
+val head_evar : evar_map -> constr -> existential_key (** may raise NoHeadEvar *)
 
 (* Expand head evar if any *)
-val whd_head_evar :  evar_map -> EConstr.constr -> EConstr.constr
+val whd_head_evar :  evar_map -> constr -> constr
 
 (* An over-approximation of [has_undefined (nf_evars evd c)] *)
-val has_undefined_evars : evar_map -> EConstr.constr -> bool
+val has_undefined_evars : evar_map -> constr -> bool
 
-val is_ground_term :  evar_map -> EConstr.constr -> bool
+val is_ground_term :  evar_map -> constr -> bool
 val is_ground_env  :  evar_map -> env -> bool
 
 (** [gather_dependent_evars evm seeds] classifies the evars in [evm]
@@ -121,14 +122,14 @@ val advance : evar_map -> evar -> evar option
     This is roughly a combination of the previous functions and
     [nf_evar]. *)
 
-val undefined_evars_of_term : evar_map -> EConstr.constr -> Evar.Set.t
+val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
 val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
 val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
 
 (** [occur_evar_upto sigma k c] returns [true] if [k] appears in
     [c]. It looks up recursively in [sigma] for the value of existential
     variables. *)
-val occur_evar_upto : evar_map -> Evar.t -> EConstr.t -> bool
+val occur_evar_upto : evar_map -> Evar.t -> constr -> bool
 
 (** {6 Value/Type constraints} *)
 
@@ -139,18 +140,18 @@ val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
 (** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
     uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
 
-val whd_evar :  evar_map -> EConstr.constr -> EConstr.constr
-val nf_evar :  evar_map -> EConstr.constr -> EConstr.constr
-val j_nf_evar :  evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment
+val whd_evar :  evar_map -> constr -> constr
+val nf_evar :  evar_map -> constr -> constr
+val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment
 val jl_nf_evar :
-   evar_map -> EConstr.unsafe_judgment list -> EConstr.unsafe_judgment list
+   evar_map -> unsafe_judgment list -> unsafe_judgment list
 val jv_nf_evar :
-   evar_map -> EConstr.unsafe_judgment array -> EConstr.unsafe_judgment array
+   evar_map -> unsafe_judgment array -> unsafe_judgment array
 val tj_nf_evar :
-   evar_map -> EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment
+   evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
 val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
-val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t
+val nf_rel_context_evar : evar_map -> rel_context -> rel_context
 val nf_env_evar : evar_map -> env -> env
 
 val nf_evar_info : evar_map -> evar_info -> evar_info
@@ -159,39 +160,39 @@ val nf_evar_map_undefined : evar_map -> evar_map
 
 (** Presenting terms without solved evars *)
 
-val nf_evars_universes : evar_map -> constr -> constr
+val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr
 
-val nf_evars_and_universes : evar_map -> evar_map * (constr -> constr)
-val e_nf_evars_and_universes : evar_map ref -> (constr -> constr) * Universes.universe_opt_subst
+val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
+val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst
 
 (** Normalize the evar map w.r.t. universes, after simplification of constraints.
     Return the substitution function for constrs as well. *)
-val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
+val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
 
 (** Replacing all evars, possibly raising [Uninstantiated_evar] *)
 exception Uninstantiated_evar of existential_key
-val flush_and_check_evars :  evar_map -> EConstr.constr -> constr
+val flush_and_check_evars :  evar_map -> constr -> Constr.constr
 
 (** {6 Term manipulation up to instantiation} *)
 
 (** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
     as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
     value of [e] in [sigma] is (recursively) used. *)
-val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
+val kind_of_term_upto : evar_map -> Constr.constr -> (Constr.constr,Constr.types) kind_of_term
 
 (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
     [u] up to existential variable instantiation and equalisable
     universes. The term [t] is interpreted in [sigma1] while [u] is
     interpreted in [sigma2]. The universe constraints in [sigma2] are
     assumed to be an extention of those in [sigma1]. *)
-val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool
 
 (** {6 Removing hyps in evars'context}
 raise OccurHypInSimpleClause if the removal breaks dependencies *)
 
 type clear_dependency_error =
 | OccurHypInSimpleClause of Id.t option
-| EvarTypingBreak of existential
+| EvarTypingBreak of Constr.existential
 
 exception ClearDependencyError of Id.t * clear_dependency_error
 
@@ -199,7 +200,7 @@ exception ClearDependencyError of Id.t * clear_dependency_error
     used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
 val cleared : bool Store.field
 
-val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> EConstr.types ->
+val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
   Id.Set.t -> named_context_val * types
 
 val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
@@ -208,19 +209,19 @@ val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> ty
 type csubst
 
 val empty_csubst : csubst
-val csubst_subst : csubst -> EConstr.t -> EConstr.t
+val csubst_subst : csubst -> constr -> constr
 
 type ext_named_context =
-  csubst * (Id.t * EConstr.constr) list *
-  Id.Set.t * Context.Named.t
+  csubst * (Id.t * constr) list *
+  Id.Set.t * named_context
 
 val push_rel_decl_to_named_context :
-  Context.Rel.Declaration.t -> ext_named_context -> ext_named_context
+  rel_declaration -> ext_named_context -> ext_named_context
 
-val push_rel_context_to_named_context : Environ.env -> EConstr.types ->
-  named_context_val * EConstr.types * EConstr.constr list * csubst * (identifier*EConstr.constr) list
+val push_rel_context_to_named_context : Environ.env -> types ->
+  named_context_val * types * constr list * csubst * (identifier*constr) list
 
-val generalize_evar_over_rels : evar_map -> EConstr.existential -> EConstr.types * EConstr.constr list
+val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 
 (** Evar combinators *)
 
@@ -235,5 +236,5 @@ val meta_counter_summary_name : string
 
 (** Deprecater *)
 
-type type_constraint = EConstr.types option
-type val_constraint = EConstr.constr option
+type type_constraint = types option
+type val_constraint = constr option
diff --git a/engine/proofview.ml b/engine/proofview.ml
index ab72cc405..0a18cf191 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -995,7 +995,7 @@ module Goal = struct
 
   let env { env=env } = env
   let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma
-  let hyps { env=env } = Environ.named_context env
+  let hyps { env=env } = EConstr.named_context env
   let concl { concl=concl } = concl
   let extra { sigma=sigma; self=self } = goal_extra sigma self
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 9f10e874a..025e3de20 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -14,6 +14,7 @@
 
 open Util
 open Term
+open EConstr
 
 (** Main state of tactics *)
 type proofview
@@ -43,7 +44,7 @@ val compact : entry -> proofview -> entry * proofview
     empty [evar_map] (indeed a proof can be triggered by an incomplete
     pretyping), [init] takes an additional argument to represent the
     initial [evar_map]. *)
-val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofview
+val init : Evd.evar_map -> (Environ.env * types) list -> entry * proofview
 
 (** A [telescope] is a list of environment and conclusion like in
     {!init}, except that each element may depend on the previous
@@ -52,7 +53,7 @@ val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofvi
     [evar_map] is threaded in state passing style. *)
 type telescope =
   | TNil of Evd.evar_map
-  | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
+  | TCons of Environ.env * Evd.evar_map * types * (Evd.evar_map -> constr -> telescope)
 
 (** Like {!init}, but goals are allowed to be dependent on one
     another. Dependencies between goals is represented with the type
@@ -69,8 +70,8 @@ val finished : proofview -> bool
 (** Returns the current [evar] state. *)
 val return : proofview -> Evd.evar_map
 
-val partial_proof : entry -> proofview -> EConstr.constr list
-val initial_goals : entry -> (EConstr.constr * EConstr.types) list
+val partial_proof : entry -> proofview -> constr list
+val initial_goals : entry -> (constr * types) list
 
 
 
@@ -484,15 +485,15 @@ module Goal : sig
       respectively the conclusion of [gl], the hypotheses of [gl], the
       environment of [gl] (i.e. the global environment and the
       hypotheses) and the current evar map. *)
-  val concl : ([ `NF ], 'r) t -> EConstr.constr
-  val hyps : ([ `NF ], 'r) t -> Context.Named.t
+  val concl : ([ `NF ], 'r) t -> constr
+  val hyps : ([ `NF ], 'r) t -> named_context
   val env : ('a, 'r) t -> Environ.env
   val sigma : ('a, 'r) t -> 'r Sigma.t
   val extra : ('a, 'r) t -> Evd.Store.t
 
   (** Returns the goal's conclusion even if the goal is not
       normalised. *)
-  val raw_concl : ('a, 'r) t -> EConstr.constr
+  val raw_concl : ('a, 'r) t -> constr
 
   type ('a, 'b) enter =
     { enter : 'r. ('a, 'r) t -> 'b }
diff --git a/engine/termops.ml b/engine/termops.ml
index 46e9ad927..c35e92f97 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -167,19 +167,10 @@ let rel_list n m =
   in
   reln [] 1
 
-let local_assum (na, t) =
-  let open RelDecl in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let open RelDecl in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 let push_rel_assum (x,t) env =
   let open RelDecl in
-  push_rel (local_assum (x,t)) env
+  let open EConstr in
+  push_rel (LocalAssum (x,t)) env
 
 let push_rels_assum assums =
   let open RelDecl in
@@ -218,8 +209,8 @@ let mkProd_wo_LetIn decl c =
   let open EConstr in
   let open RelDecl in
   match decl with
-    | LocalAssum (na,t) -> mkProd (na, EConstr.of_constr t, c)
-    | LocalDef (_,b,_) -> Vars.subst1 (EConstr.of_constr b) c
+    | LocalAssum (na,t) -> mkProd (na, t, c)
+    | LocalDef (_,b,_) -> Vars.subst1 b c
 
 let it_mkProd init = List.fold_left (fun c (n,t)  -> EConstr.mkProd (n, t, c)) init
 let it_mkLambda init = List.fold_left (fun c (n,t)  -> EConstr.mkLambda (n, t, c)) init
@@ -334,7 +325,8 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
 
 let fold_rec_types g (lna,typarray,_) e =
   let open EConstr in
-  let ctxt = Array.map2_i (fun i na t -> local_assum (na, Vars.lift i t)) lna typarray in
+  let open Vars in
+  let ctxt = Array.map2_i (fun i na t -> RelDecl.LocalAssum (na, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> g assum e) e ctxt
 
 let map_left2 f a g b =
@@ -350,6 +342,7 @@ let map_left2 f a g b =
   end
 
 let map_constr_with_binders_left_to_right sigma g f l c =
+  let open RelDecl in
   let open EConstr in
   match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -361,18 +354,18 @@ let map_constr_with_binders_left_to_right sigma g f l c =
       else mkCast (b',k,t')
   | Prod (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (local_assum (na,t)) l) b in
+      let b' = f (g (LocalAssum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkProd (na, t', b')
   | Lambda (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (local_assum (na,t)) l) b in
+      let b' = f (g (LocalAssum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkLambda (na, t', b')
   | LetIn (na,bo,t,b) ->
       let bo' = f l bo in
       let t' = f l t in
-      let b' = f (g (local_def (na,bo,t)) l) b in
+      let b' = f (g (LocalDef (na,bo,t)) l) b in
 	if bo' == bo && t' == t && b' == b then c
 	else mkLetIn (na, bo', t', b')	    
   | App (c,[||]) -> assert false
@@ -414,7 +407,6 @@ let map_constr_with_binders_left_to_right sigma g f l c =
 
 (* strong *)
 let map_constr_with_full_binders sigma g f l cstr =
-  let inj c = EConstr.Unsafe.to_constr c in
   let open EConstr in
   let open RelDecl in
   match EConstr.kind sigma cstr with
@@ -426,16 +418,16 @@ let map_constr_with_full_binders sigma g f l cstr =
       if c==c' && t==t' then cstr else mkCast (c', k, t')
   | Prod (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (LocalAssum (na, inj t)) l) c in
+      let c' = f (g (LocalAssum (na, t)) l) c in
       if t==t' && c==c' then cstr else mkProd (na, t', c')
   | Lambda (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (LocalAssum (na, inj t)) l) c in
+      let c' = f (g (LocalAssum (na, t)) l) c in
       if t==t' && c==c' then cstr else  mkLambda (na, t', c')
   | LetIn (na,b,t,c) ->
       let b' = f l b in
       let t' = f l t in
-      let c' = f (g (LocalDef (na, inj b, inj t)) l) c in
+      let c' = f (g (LocalDef (na, b, t)) l) c in
       if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
   | App (c,al) ->
       let c' = f l c in
@@ -456,7 +448,7 @@ let map_constr_with_full_binders sigma g f l cstr =
   | Fix (ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (LocalAssum (na, inj t)) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -464,7 +456,7 @@ let map_constr_with_full_binders sigma g f l cstr =
   | CoFix(ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (LocalAssum (na, inj t)) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -577,10 +569,10 @@ let occur_var env sigma id c =
 let occur_var_in_decl env sigma hyp decl =
   let open NamedDecl in
   match decl with
-    | LocalAssum (_,typ) -> occur_var env sigma hyp (EConstr.of_constr typ)
+    | LocalAssum (_,typ) -> occur_var env sigma hyp typ
     | LocalDef (_, body, typ) ->
-        occur_var env sigma hyp (EConstr.of_constr typ) ||
-        occur_var env sigma hyp (EConstr.of_constr body)
+        occur_var env sigma hyp typ ||
+        occur_var env sigma hyp body
 
 let local_occur_var sigma id c =
   let rec occur c = match EConstr.kind sigma c with
@@ -655,8 +647,8 @@ let dependent_univs_no_evar sigma c t = dependent_main true true sigma c t
 let dependent_in_decl sigma a decl =
   let open NamedDecl in
   match decl with
-    | LocalAssum (_,t) -> dependent sigma a (EConstr.of_constr t)
-    | LocalDef (_, body, t) -> dependent sigma a (EConstr.of_constr body) || dependent sigma a (EConstr.of_constr t)
+    | LocalAssum (_,t) -> dependent sigma a t
+    | LocalDef (_, body, t) -> dependent sigma a body || dependent sigma a t
 
 let count_occurrences sigma m t =
   let open EConstr in
@@ -886,7 +878,7 @@ let eq_constr sigma t1 t2 = constr_cmp sigma Reduction.CONV t1 t2
 
 (* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn)
    App(c,[||]) -> ([],c) *)
-let split_app c = match kind_of_term c with
+let split_app sigma c = match EConstr.kind sigma c with
     App(c,l) ->
       let len = Array.length l in
       if Int.equal len 0 then ([],c) else
@@ -895,28 +887,30 @@ let split_app c = match kind_of_term c with
 	c::(Array.to_list prev), last
   | _ -> assert false
 
-type subst = (Context.Rel.t * constr) Evar.Map.t
+type subst = (EConstr.rel_context * EConstr.constr) Evar.Map.t
 
 exception CannotFilter
 
 let filtering sigma env cv_pb c1 c2 =
+  let open EConstr in
+  let open Vars in
   let evm = ref Evar.Map.empty in
   let define cv_pb e1 ev c1 =
     try let (e2,c2) = Evar.Map.find ev !evm in
     let shift = List.length e1 - List.length e2 in
-    if constr_cmp sigma cv_pb (EConstr.of_constr c1) (EConstr.of_constr (lift shift c2)) then () else raise CannotFilter
+    if constr_cmp sigma cv_pb c1 (lift shift c2) then () else raise CannotFilter
     with Not_found ->
       evm := Evar.Map.add ev (e1,c1) !evm
   in
   let rec aux env cv_pb c1 c2 =
-    match kind_of_term c1, kind_of_term c2 with
+    match EConstr.kind sigma c1, EConstr.kind sigma c2 with
       | App _, App _ ->
-        let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in
+        let ((p1,l1),(p2,l2)) = (split_app sigma c1),(split_app sigma c2) in
         let () = aux env cv_pb l1 l2 in
         begin match p1, p2 with
         | [], [] -> ()
         | (h1 :: p1), (h2 :: p2) ->
-          aux env cv_pb (applistc h1 p1) (applistc h2 p2)
+          aux env cv_pb (applist (h1, p1)) (applist (h2, p2))
         | _ -> assert false
         end
       | Prod (n,t1,c1), Prod (_,t2,c2) ->
@@ -925,21 +919,20 @@ let filtering sigma env cv_pb c1 c2 =
       | _, Evar (ev,_) -> define cv_pb env ev c1
       | Evar (ev,_), _ -> define cv_pb env ev c2
       | _ ->
-          let inj = EConstr.Unsafe.to_constr in
 	  if compare_constr_univ sigma
-	  (fun pb c1 c2 -> aux env pb (inj c1) (inj c2); true) cv_pb (EConstr.of_constr c1) (EConstr.of_constr c2) then ()
+	  (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
 	  else raise CannotFilter
 	  (* TODO: le reste des binders *)
   in
   aux env cv_pb c1 c2; !evm
 
 let decompose_prod_letin sigma c =
-  let rec prodec_rec i l sigma c = match EConstr.kind sigma c with
-    | Prod (n,t,c)    -> prodec_rec (succ i) (local_assum (n, t)::l) sigma c
-    | LetIn (n,d,t,c) -> prodec_rec (succ i) (local_def (n, d, t)::l) sigma c
-    | Cast (c,_,_)    -> prodec_rec i l sigma c
-    | _               -> i,l, c in
-  prodec_rec 0 [] sigma c
+  let rec prodec_rec i l c = match EConstr.kind sigma c with
+    | Prod (n,t,c)    -> prodec_rec (succ i) (RelDecl.LocalAssum (n,t)::l) c
+    | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n,d,t)::l) c
+    | Cast (c,_,_)    -> prodec_rec i l c
+    | _               -> i,l,c in
+  prodec_rec 0 [] c
 
 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
  * gives n (casts are ignored) *)
@@ -1007,7 +1000,7 @@ let rec eta_reduce_head sigma c =
 (* iterator on rel context *)
 let process_rel_context f env =
   let sign = named_context_val env in
-  let rels = rel_context env in
+  let rels = EConstr.rel_context env in
   let env0 = reset_with_named_context sign env in
   Context.Rel.fold_outside f rels ~init:env0
 
@@ -1055,6 +1048,14 @@ let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 let mem_named_context_val id ctxt =
   try Environ.lookup_named_val id ctxt; true with Not_found -> false
 
+let map_rel_decl f = function
+| RelDecl.LocalAssum (id, t) -> RelDecl.LocalAssum (id, f t)
+| RelDecl.LocalDef (id, b, t) -> RelDecl.LocalDef (id, f b, f t)
+
+let map_named_decl f = function
+| NamedDecl.LocalAssum (id, t) -> NamedDecl.LocalAssum (id, f t)
+| NamedDecl.LocalDef (id, b, t) -> NamedDecl.LocalDef (id, f b, f t)
+
 let compact_named_context sign =
   let compact l decl =
     match decl, l with
@@ -1098,10 +1099,10 @@ let global_vars_set env sigma constr =
 let global_vars env sigma ids = Id.Set.elements (global_vars_set env sigma ids)
 
 let global_vars_set_of_decl env sigma = function
-  | NamedDecl.LocalAssum (_,t) -> global_vars_set env sigma (EConstr.of_constr t)
+  | NamedDecl.LocalAssum (_,t) -> global_vars_set env sigma t
   | NamedDecl.LocalDef (_,c,t) ->
-      Id.Set.union (global_vars_set env sigma (EConstr.of_constr t))
-        (global_vars_set env sigma (EConstr.of_constr c))
+      Id.Set.union (global_vars_set env sigma t)
+        (global_vars_set env sigma c)
 
 let dependency_closure env sigma sign hyps =
   if Id.Set.is_empty hyps then [] else
@@ -1155,6 +1156,7 @@ let context_chop k ctx =
 
 (* Do not skip let-in's *)
 let env_rel_context_chop k env =
+  let open EConstr in
   let rels = rel_context env in
   let ctx1,ctx2 = List.chop k rels in
   push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
diff --git a/engine/termops.mli b/engine/termops.mli
index 196962354..841de34b1 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -34,7 +34,7 @@ val push_rel_assum : Name.t * types -> env -> env
 val push_rels_assum : (Name.t * Constr.types) list -> env -> env
 val push_named_rec_types : Name.t array * Constr.types array * 'a -> env -> env
 
-val lookup_rel_id : Id.t -> Context.Rel.t -> int * Constr.constr option * Constr.types
+val lookup_rel_id : Id.t -> ('c, 't) Context.Rel.pt -> int * 'c option * 't
 (** Associates the contents of an identifier in a [rel_context]. Raise
     [Not_found] if there is no such identifier. *)
 
@@ -45,16 +45,16 @@ val rel_vect : int -> int -> Constr.constr array
 val rel_list : int -> int -> constr list
 
 (** iterators/destructors on terms *)
-val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
-val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkProd_or_LetIn : rel_declaration -> types -> types
+val mkProd_wo_LetIn : rel_declaration -> types -> types
 val it_mkProd : types -> (Name.t * types) list -> types
 val it_mkLambda : constr -> (Name.t * types) list -> constr
-val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
-val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types
+val it_mkProd_or_LetIn : types -> rel_context -> types
+val it_mkProd_wo_LetIn : types -> rel_context -> types
 val it_mkLambda_or_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr
-val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types
+val it_mkNamedProd_or_LetIn : types -> named_context -> types
 val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types
-val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr
+val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
 
 (* Ad hoc version reinserting letin, assuming the body is defined in
    the context where the letins are expanded *)
@@ -64,12 +64,12 @@ val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Const
 
 val map_constr_with_binders_left_to_right :
   Evd.evar_map ->
-  (Context.Rel.Declaration.t -> 'a -> 'a) ->
+  (rel_declaration -> 'a -> 'a) ->
   ('a -> constr -> constr) ->
     'a -> constr -> constr
 val map_constr_with_full_binders :
   Evd.evar_map ->
-  (Context.Rel.Declaration.t -> 'a -> 'a) ->
+  (rel_declaration -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
 
 (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
@@ -105,7 +105,7 @@ val occur_evar : Evd.evar_map -> existential_key -> constr -> bool
 val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
 val occur_var_in_decl :
   env -> Evd.evar_map ->
-  Id.t -> Context.Named.Declaration.t -> bool
+  Id.t -> named_declaration -> bool
 
 (** As {!occur_var} but assume the identifier not to be a section variable *)
 val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool
@@ -117,7 +117,7 @@ val dependent : Evd.evar_map -> constr -> constr -> bool
 val dependent_no_evar : Evd.evar_map -> constr -> constr -> bool
 val dependent_univs : Evd.evar_map -> constr -> constr -> bool
 val dependent_univs_no_evar : Evd.evar_map -> constr -> constr -> bool
-val dependent_in_decl : Evd.evar_map -> constr -> Context.Named.Declaration.t -> bool
+val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool
 val count_occurrences : Evd.evar_map -> constr -> constr -> int
 val collect_metas : Evd.evar_map -> constr -> int list
 val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
@@ -182,11 +182,11 @@ exception CannotFilter
    (context,term), or raises [CannotFilter].
    Warning: Outer-kernel sort subtyping are taken into account: c1 has
    to be smaller than c2 wrt. sorts. *)
-type subst = (Context.Rel.t * Constr.constr) Evar.Map.t
-val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> Constr.constr -> Constr.constr -> subst
+type subst = (rel_context * constr) Evar.Map.t
+val filtering : Evd.evar_map -> rel_context -> Reduction.conv_pb -> constr -> constr -> subst
 
-val decompose_prod_letin : Evd.evar_map -> constr -> int * Context.Rel.t * constr
-val align_prod_letin : Evd.evar_map -> constr -> constr -> Context.Rel.t * constr
+val decompose_prod_letin : Evd.evar_map -> constr -> int * rel_context * constr
+val align_prod_letin : Evd.evar_map -> constr -> constr -> rel_context * constr
 
 (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
    gives {% $ %}n{% $ %} (casts are ignored) *)
@@ -215,8 +215,8 @@ val add_name : Name.t -> names_context -> names_context
 val lookup_name_of_rel : int -> names_context -> Name.t
 val lookup_rel_of_name : Id.t -> names_context -> int
 val empty_names_context : names_context
-val ids_of_rel_context : Context.Rel.t -> Id.t list
-val ids_of_named_context : Context.Named.t -> Id.t list
+val ids_of_rel_context : ('c, 't) Context.Rel.pt -> Id.t list
+val ids_of_named_context : ('c, 't) Context.Named.pt -> Id.t list
 val ids_of_context : env -> Id.t list
 val names_of_rel_context : env -> names_context
 
@@ -228,15 +228,15 @@ val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t
 (* [env_rel_context_chop n env] extracts out the [n] top declarations
    of the rel_context part of [env], counting both local definitions and
    hypotheses *)
-val env_rel_context_chop : int -> env -> env * Context.Rel.t
+val env_rel_context_chop : int -> env -> env * rel_context
 
 (** Set of local names *)
 val vars_of_env: env -> Id.Set.t
 val add_vname : Id.Set.t -> Name.t -> Id.Set.t
 
 (** other signature iterators *)
-val process_rel_context : (Context.Rel.Declaration.t -> env -> env) -> env -> env
-val assums_of_rel_context : Context.Rel.t -> (Name.t * Constr.constr) list
+val process_rel_context : (rel_declaration -> env -> env) -> env -> env
+val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t * 't) list
 val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t
 val substl_rel_context : Constr.constr list -> Context.Rel.t -> Context.Rel.t
 val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *)
@@ -244,23 +244,26 @@ val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in contex
 val map_rel_context_in_env :
   (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t
 val map_rel_context_with_binders :
-  (int -> Constr.constr -> Constr.constr) -> Context.Rel.t -> Context.Rel.t
+  (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt
 val fold_named_context_both_sides :
   ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) ->
     Context.Named.t -> init:'a -> 'a
 val mem_named_context_val : Id.t -> named_context_val -> bool
 val compact_named_context : Context.Named.t -> Context.Compacted.t
 
+val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt
+val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt
+
 val clear_named_body : Id.t -> env -> env
 
 val global_vars : env -> Evd.evar_map -> constr -> Id.t list
 val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t
-val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t
+val global_vars_set_of_decl : env -> Evd.evar_map -> named_declaration -> Id.Set.t
 val global_app_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses * constr option
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
-val dependency_closure : env -> Evd.evar_map -> Context.Named.t -> Id.Set.t -> Id.t list
+val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.t list
 
 (** Test if an identifier is the basename of a global reference *)
 val is_section_variable : Id.t -> bool