CLEANUP: Context.{Rel,Named}.Declaration.t

20 files changed, 716 insertions, 439 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 9bc67b5adb..4476fe5241 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -245,10 +245,12 @@ and 'a infos = {
 let info_flags info = info.i_flags
 let info_env info = info.i_cache.i_env
 
+open Context.Named.Declaration
+
 let rec assoc_defined id = function
 | [] -> raise Not_found
-| (_, None, _) :: ctxt -> assoc_defined id ctxt
-| (id', Some c, _) :: ctxt ->
+| LocalAssum _ :: ctxt -> assoc_defined id ctxt
+| LocalDef (id', c, _) :: ctxt ->
   if Id.equal id id' then c else assoc_defined id ctxt
 
 let ref_value_cache ({i_cache = cache} as infos)  ref =
@@ -285,9 +287,10 @@ let defined_rels flags env =
   let ctx = rel_context env in
   let len = List.length ctx in
   let ans = Array.make len None in
-  let iter i (_, b, _) = match b with
-  | None -> ()
-  | Some _ -> Array.unsafe_set ans i b
+  let open Context.Rel.Declaration in
+  let iter i = function
+    | LocalAssum _ -> ()
+    | LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b)
   in
   let () = List.iteri iter ctx in
   ans
diff --git a/kernel/context.ml b/kernel/context.ml
index 3be1e83230..4e53b73a28 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -32,215 +32,391 @@ open Names
 (** Representation of contexts that can capture anonymous as well as non-anonymous variables.
     Individual declarations are then designated by de Bruijn indexes. *)
 module Rel =
+struct
+  (** Representation of {e local declarations}. *)
+  module Declaration =
   struct
-    (** Representation of {e local declarations}.
-
-        [(name, None, typ)] represents a {e local assumption}.
-        In the Reference Manual we denote them as [(name:typ)].
-
-        [(name, Some value, typ)] represents a {e local definition}.
-        In the Reference Manual we denote them as [(name := value : typ)].
-    *)
-    module Declaration =
-      struct
-	type t = Name.t * Constr.t option * Constr.t
-
-	(** Map all terms in a given declaration. *)
-	let map f (n, v, ty) = (n, Option.map f v, f ty)
-
-	(** Reduce all terms in a given declaration to a single value. *)
-	let fold f (_, v, ty) a = f ty (Option.fold_right f v a)
-
-	(** Check whether any term in a given declaration satisfies a given predicate. *)
-	let exists f (_, v, ty) = Option.cata f false v || f ty
-
-	(** Check whether all terms in a given declaration satisfy a given predicate. *)
-	let for_all f (_, v, ty) = Option.cata f true v && f ty
-
-	(** Check whether the two given declarations are equal. *)
-	let equal (n1, v1, ty1) (n2, v2, ty2) =
-	  Name.equal n1 n2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2
-      end
-
-    (** Rel-context is represented as a list of declarations.
-        Inner-most declarations are at the beginning of the list.
-        Outer-most declarations are at the end of the list. *)
-    type t = Declaration.t list
-
-    (** empty rel-context *)
-    let empty = []
-
-    (** Return a new rel-context enriched by with a given inner-most declaration. *)
-    let add d ctx = d :: ctx
-
-    (** Return a declaration designated by a given de Bruijn index.
-        @raise Not_found if the designated de Bruijn index is not present in the designated rel-context. *)
-    let rec lookup n ctx =
-      match n, ctx with
-      | 1, decl :: _ -> decl
-      | n, _ :: sign -> lookup (n-1) sign
-      | _, []        -> raise Not_found
-
-    (** Map all terms in a given rel-context. *)
-    let map f =
-      let map_decl (n, body_o, typ as decl) =
-	let body_o' = Option.smartmap f body_o in
-	let typ' = f typ in
-	if body_o' == body_o && typ' == typ then decl else
-          (n, body_o', typ')
-      in
-      List.smartmap map_decl
-
-    (** Reduce all terms in a given rel-context to a single value.
-        Innermost declarations are processed first. *)
-    let fold_inside f ~init = List.fold_left f init
-
-    (** Reduce all terms in a given rel-context to a single value.
-        Outermost declarations are processed first. *)
-    let fold_outside f l ~init = List.fold_right f l init
-
-    (** Perform a given action on every declaration in a given rel-context. *)
-    let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
-
-    (** Return the number of {e local declarations} in a given context. *)
-    let length = List.length
-
-    (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
-        with n = |Δ| and with the local definitions of [Γ] skipped in
-        [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
-    let nhyps =
-      let rec nhyps acc = function
-	| [] -> acc
-	| (_,None,_)::hyps -> nhyps (1+acc) hyps
-	| (_,Some _,_)::hyps -> nhyps acc hyps in
-      nhyps 0
-
-    (** Map a given rel-context to a list where each {e local assumption} is mapped to [true]
-        and each {e local definition} is mapped to [false]. *)
-    let to_tags =
-      let rec aux l = function
-	| [] -> l
-	| (_,Some _,_)::ctx -> aux (true::l) ctx
-	| (_,None,_)::ctx -> aux (false::l) ctx
-      in aux []
-
-    (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
-        with n = |Δ| and with the {e local definitions} of [Γ] skipped in
-        [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
-    let to_extended_list n =
-      let rec reln l p = function
-	| (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
-	| (_, Some _, _) :: hyps -> reln l (p+1) hyps
-	| [] -> l
-      in
-      reln [] 1
-
-    (** [extended_vect n Γ] does the same, returning instead an array. *)
-    let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps)
+    (* local declaration *)
+    type t =
+      | LocalAssum of Name.t * Constr.t            (** name, type *)
+      | LocalDef of Name.t * Constr.t * Constr.t   (** name, value, type *)
+
+    (** Return the name bound by a given declaration. *)
+    let get_name = function
+      | LocalAssum (na,_)
+      | LocalDef (na,_,_) -> na
+
+    (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+    let get_value = function
+      | LocalAssum _ -> None
+      | LocalDef (_,v,_) -> Some v
+                                 
+    (** Return the type of the name bound by a given declaration. *)
+    let get_type = function
+      | LocalAssum (_,ty)
+      | LocalDef (_,_,ty) -> ty
+                               
+    (** Set the name that is bound by a given declaration. *)
+    let set_name na = function
+      | LocalAssum (_,ty) -> LocalAssum (na, ty)
+      | LocalDef (_,v,ty) -> LocalDef (na, v, ty)
+
+    (** Set the type of the bound variable in a given declaration. *)
+    let set_type ty = function
+      | LocalAssum (na,_) -> LocalAssum (na, ty)
+      | LocalDef (na,v,_) -> LocalDef (na, v, ty)
+
+    (** Return [true] iff a given declaration is a local assumption. *)
+    let is_local_assum = function
+      | LocalAssum _ -> true
+      | LocalDef _ -> false
+
+    (** Return [true] iff a given declaration is a local definition. *)
+    let is_local_def = function
+      | LocalAssum _ -> false
+      | LocalDef _ -> true
+
+    (** Check whether any term in a given declaration satisfies a given predicate. *)
+    let exists f = function
+      | LocalAssum (_, ty) -> f ty
+      | LocalDef (_, v, ty) -> f v || f ty
+
+      (** Check whether all terms in a given declaration satisfy a given predicate. *)
+    let for_all f = function
+      | LocalAssum (_, ty) -> f ty
+      | LocalDef (_, v, ty) -> f v && f ty
+
+    (** Check whether the two given declarations are equal. *)
+    let equal decl1 decl2 =
+      match decl1, decl2 with
+      | LocalAssum (n1,ty1), LocalAssum (n2, ty2) ->
+          Name.equal n1 n2 && Constr.equal ty1 ty2
+      | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) ->
+          Name.equal n1 n2 && Constr.equal v1 v2 && Constr.equal ty1 ty2
+      | _ ->
+          false
+
+    (** Map the name bound by a given declaration. *)
+    let map_name f = function
+      | LocalAssum (na, ty) as decl ->
+          let na' = f na in
+          if na == na' then decl else LocalAssum (na', ty)
+      | LocalDef (na, v, ty) as decl ->
+          let na' = f na in
+          if na == na' then decl else LocalDef (na', v, ty)
+
+    (** For local assumptions, this function returns the original local assumptions.
+        For local definitions, this function maps the value in the local definition. *)
+    let map_value f = function
+      | LocalAssum _ as decl -> decl
+      | LocalDef (na, v, t) as decl ->
+          let v' = f v in
+          if v == v' then decl else LocalDef (na, v', t)
+
+    (** Map the type of the name bound by a given declaration. *)
+    let map_type f = function
+      | LocalAssum (na, ty) as decl ->
+          let ty' = f ty in
+          if ty == ty' then decl else LocalAssum (na, ty')
+      | LocalDef (na, v, ty) as decl ->         
+          let ty' = f ty in
+          if ty == ty' then decl else LocalDef (na, v, ty')
+
+    (** Map all terms in a given declaration. *)
+    let map_constr f = function
+      | LocalAssum (na, ty) as decl ->
+          let ty' = f ty in
+          if ty == ty' then decl else LocalAssum (na, ty')
+      | LocalDef (na, v, ty) as decl ->
+          let v' = f v in
+          let ty' = f ty in
+          if v == v' && ty == ty' then decl else LocalDef (na, v', ty')
+
+    (** Perform a given action on all terms in a given declaration. *)
+    let iter_constr f = function
+      | LocalAssum (_,ty) -> f ty
+      | LocalDef (_,v,ty) -> f v; f ty
+
+    (** Reduce all terms in a given declaration to a single value. *)
+    let fold f decl acc =
+      match decl with
+      | LocalAssum (n,ty) -> f ty acc
+      | LocalDef (n,v,ty) -> f ty (f v acc)
+
+    let to_tuple = function
+      | LocalAssum (na, ty) -> na, None, ty
+      | LocalDef (na, v, ty) -> na, Some v, ty
+
+    let of_tuple = function
+      | n, None, ty -> LocalAssum (n,ty)
+      | n, Some v, ty -> LocalDef (n,v,ty)
   end
 
+  (** Rel-context is represented as a list of declarations.
+      Inner-most declarations are at the beginning of the list.
+      Outer-most declarations are at the end of the list. *)
+  type t = Declaration.t list
+
+  (** empty rel-context *)
+  let empty = []
+
+  (** Return a new rel-context enriched by with a given inner-most declaration. *)
+  let add d ctx = d :: ctx
+
+  (** Return the number of {e local declarations} in a given context. *)
+  let length = List.length
+
+  (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+      with n = |Δ| and with the local definitions of [Γ] skipped in
+      [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+  let nhyps =
+    let open Declaration in
+    let rec nhyps acc = function
+      | [] -> acc
+      | LocalAssum _ :: hyps -> nhyps (succ acc) hyps
+      | LocalDef _ :: hyps -> nhyps acc hyps
+    in
+    nhyps 0
+
+  (** Return a declaration designated by a given de Bruijn index.
+      @raise Not_found if the designated de Bruijn index is not present in the designated rel-context. *)
+  let rec lookup n ctx =
+    match n, ctx with
+    | 1, decl :: _ -> decl
+    | n, _ :: sign -> lookup (n-1) sign
+    | _, []        -> raise Not_found
+
+  (** Check whether given two rel-contexts are equal. *)
+  let equal = List.equal Declaration.equal
+
+  (** Map all terms in a given rel-context. *)
+  let map f = List.smartmap (Declaration.map_constr f)
+
+  (** Perform a given action on every declaration in a given rel-context. *)
+  let iter f = List.iter (Declaration.iter_constr f)
+
+  (** Reduce all terms in a given rel-context to a single value.
+      Innermost declarations are processed first. *)
+  let fold_inside f ~init = List.fold_left f init
+
+  (** Reduce all terms in a given rel-context to a single value.
+      Outermost declarations are processed first. *)
+  let fold_outside f l ~init = List.fold_right f l init
+
+  (** Map a given rel-context to a list where each {e local assumption} is mapped to [true]
+      and each {e local definition} is mapped to [false]. *)
+  let to_tags =
+    let rec aux l = function
+      | [] -> l
+      | Declaration.LocalDef _ :: ctx -> aux (true::l) ctx
+      | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx
+    in aux []
+
+  (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+      with n = |Δ| and with the {e local definitions} of [Γ] skipped in
+      [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+  let to_extended_list n =
+    let rec reln l p = function
+      | Declaration.LocalAssum _ :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
+      | Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps
+      | [] -> l
+    in
+    reln [] 1
+
+  (** [extended_vect n Γ] does the same, returning instead an array. *)
+  let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps)
+end
+
 (** This module represents contexts that can capture non-anonymous variables.
     Individual declarations are then designated by the identifiers they bind. *)
 module Named =
+struct
+  (** Representation of {e local declarations}. *)
+  module Declaration =
   struct
-    (** Representation of {e local declarations}.
-
-        [(id, None, typ)] represents a {e local assumption}.
-        In the Reference Manual we denote them as [(name:typ)].
-
-        [(id, Some value, typ)] represents a {e local definition}.
-        In the Reference Manual we denote them as [(name := value : typ)].
-   *)
-    module Declaration =
-      struct
-	(** Named-context is represented as a list of declarations.
-            Inner-most declarations are at the beginning of the list.
-            Outer-most declarations are at the end of the list. *)
-	type t = Id.t * Constr.t option * Constr.t
-
-	(** Map all terms in a given declaration. *)
-	let map = Rel.Declaration.map
-
-	(** Reduce all terms in a given declaration to a single value. *)
-	let fold f (_, v, ty) a = f ty (Option.fold_right f v a)
-
-	(** Check whether any term in a given declaration satisfies a given predicate. *)
-	let exists f (_, v, ty) = Option.cata f false v || f ty
-
-	(** Check whether all terms in a given declaration satisfy a given predicate. *)
-	let for_all f (_, v, ty) = Option.cata f true v && f ty
-
-	(** Check whether the two given declarations are equal. *)
-	let equal (i1, v1, ty1) (i2, v2, ty2) =
-	  Id.equal i1 i2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2
-      end
-
-    type t = Declaration.t list
+    (** local declaration *)
+    type t =
+      | LocalAssum of Id.t * Constr.t             (** identifier, type *)
+      | LocalDef of Id.t * Constr.t * Constr.t    (** identifier, value, type *)
+
+    (** Return the identifier bound by a given declaration. *)
+    let get_id = function
+      | LocalAssum (id,_) -> id
+      | LocalDef (id,_,_) -> id
+
+    (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+    let get_value = function
+      | LocalAssum _ -> None
+      | LocalDef (_,v,_) -> Some v
+
+    (** Return the type of the name bound by a given declaration. *)
+    let get_type = function
+      | LocalAssum (_,ty)
+      | LocalDef (_,_,ty) -> ty
+
+    (** Set the identifier that is bound by a given declaration. *)
+    let set_id id = function
+      | LocalAssum (_,ty) -> LocalAssum (id, ty)
+      | LocalDef (_, v, ty) -> LocalDef (id, v, ty)
+
+    (** Set the type of the bound variable in a given declaration. *)
+    let set_type ty = function
+      | LocalAssum (id,_) -> LocalAssum (id, ty)
+      | LocalDef (id,v,_) -> LocalDef (id, v, ty)
+
+    (** Return [true] iff a given declaration is a local assumption. *)
+    let is_local_assum = function
+      | LocalAssum _ -> true
+      | LocalDef _ -> false
+
+    (** Return [true] iff a given declaration is a local definition. *)
+    let is_local_def = function
+      | LocalDef _ -> true
+      | LocalAssum _ -> false
+
+    (** Check whether any term in a given declaration satisfies a given predicate. *)
+    let exists f = function
+      | LocalAssum (_, ty) -> f ty
+      | LocalDef (_, v, ty) -> f v || f ty
+
+    (** Check whether all terms in a given declaration satisfy a given predicate. *)
+    let for_all f = function
+      | LocalAssum (_, ty) -> f ty
+      | LocalDef (_, v, ty) -> f v && f ty
+
+    (** Check whether the two given declarations are equal. *)
+    let equal decl1 decl2 =
+      match decl1, decl2 with
+      | LocalAssum (id1, ty1), LocalAssum (id2, ty2) ->
+          Id.equal id1 id2 && Constr.equal ty1 ty2
+      | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) ->
+          Id.equal id1 id2 && Constr.equal v1 v2 && Constr.equal ty1 ty2
+      | _ ->
+          false
+
+    (** Map the identifier bound by a given declaration. *)
+    let map_id f = function
+      | LocalAssum (id, ty) as decl ->
+          let id' = f id in
+          if id == id' then decl else LocalAssum (id', ty)
+      | LocalDef (id, v, ty) as decl ->
+          let id' = f id in
+          if id == id' then decl else LocalDef (id', v, ty)
+
+    (** For local assumptions, this function returns the original local assumptions.
+        For local definitions, this function maps the value in the local definition. *)
+    let map_value f = function
+      | LocalAssum _ as decl -> decl
+      | LocalDef (na, v, t) as decl ->
+          let v' = f v in
+          if v == v' then decl else LocalDef (na, v', t)
+
+    (** Map the type of the name bound by a given declaration. *)
+    let map_type f = function
+      | LocalAssum (id, ty) as decl ->
+          let ty' = f ty in
+          if ty == ty' then decl else LocalAssum (id, ty')
+      | LocalDef (id, v, ty) as decl ->
+          let ty' = f ty in
+          if ty == ty' then decl else LocalDef (id, v, ty')
+
+    (** Map all terms in a given declaration. *)
+    let map_constr f = function
+      | LocalAssum (id, ty) as decl ->
+          let ty' = f ty in
+          if ty == ty' then decl else LocalAssum (id, ty')
+      | LocalDef (id, v, ty) as decl ->
+          let v' = f v in
+          let ty' = f ty in
+          if v == v' && ty == ty' then decl else LocalDef (id, v', ty')
+
+    (** Perform a given action on all terms in a given declaration. *)
+    let iter_constr f = function
+      | LocalAssum (_, ty) -> f ty
+      | LocalDef (_, v, ty) -> f v; f ty
+
+    (** Reduce all terms in a given declaration to a single value. *)
+    let fold f decl a =
+      match decl with
+      | LocalAssum (_, ty) -> f ty a
+      | LocalDef (_, v, ty) -> a |> f v |> f ty
+
+    let to_tuple = function
+      | LocalAssum (id, ty) -> id, None, ty
+      | LocalDef (id, v, ty) -> id, Some v, ty
+
+    let of_tuple = function
+      | id, None, ty -> LocalAssum (id, ty)
+      | id, Some v, ty -> LocalDef (id, v, ty)
+  end
 
-    (** empty named-context *)
-    let empty = []
-
-    (** empty named-context *)
-    let add d ctx = d :: ctx
-
-    (** Return a declaration designated by a given de Bruijn index.
-        @raise Not_found if the designated identifier is not present in the designated named-context. *)
-    let rec lookup id = function
-      | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
-      | _ :: sign -> lookup id sign
-      | [] -> raise Not_found
-
-    (** Map all terms in a given named-context. *)
-    let map f =
-      let map_decl (n, body_o, typ as decl) =
-	let body_o' = Option.smartmap f body_o in
-	let typ' = f typ in
-	if body_o' == body_o && typ' == typ then decl else
-          (n, body_o', typ')
-      in
-      List.smartmap map_decl
-
-    (** Reduce all terms in a given named-context to a single value.
-        Innermost declarations are processed first. *)
-    let fold_inside f ~init = List.fold_left f init
-
-    (** Reduce all terms in a given named-context to a single value.
-        Outermost declarations are processed first. *)
-    let fold_outside f l ~init = List.fold_right f l init
-
-    (** Perform a given action on every declaration in a given named-context. *)
-    let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
-
-    (** Return the number of {e local declarations} in a given named-context. *)
-    let length = List.length
-
-    (** Check whether given two named-contexts are equal. *)
-    let equal = List.equal Declaration.equal
-
-    (** Return the set of all identifiers bound in a given named-context. *)
-    let to_vars =
-      List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty
-
-    (** [instance_from_named_context Ω] builds an instance [args] such
-        that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
-        definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
-        gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
-    let to_instance =
-      let filter = function
-	| (id, None, _) -> Some (Constr.mkVar id)
-	| (_, Some _, _) -> None
-      in
-      List.map_filter filter
+  (** Named-context is represented as a list of declarations.
+      Inner-most declarations are at the beginning of the list.
+      Outer-most declarations are at the end of the list. *)
+  type t = Declaration.t list
+
+  (** empty named-context *)
+  let empty = []
+
+  (** empty named-context *)
+  let add d ctx = d :: ctx
+
+  (** Return the number of {e local declarations} in a given named-context. *)
+  let length = List.length
+
+(** Return a declaration designated by a given de Bruijn index.
+    @raise Not_found if the designated identifier is not present in the designated named-context. *)   let rec lookup id = function
+    | decl :: _ when Id.equal id (Declaration.get_id decl) -> decl
+    | _ :: sign -> lookup id sign
+    | [] -> raise Not_found
+
+  (** Check whether given two named-contexts are equal. *)
+  let equal = List.equal Declaration.equal
+
+  (** Map all terms in a given named-context. *)
+  let map f = List.smartmap (Declaration.map_constr f)
+
+  (** Perform a given action on every declaration in a given named-context. *)
+  let iter f = List.iter (Declaration.iter_constr f)
+
+  (** Reduce all terms in a given named-context to a single value.
+      Innermost declarations are processed first. *)
+  let fold_inside f ~init = List.fold_left f init
+
+  (** Reduce all terms in a given named-context to a single value.
+      Outermost declarations are processed first. *)
+  let fold_outside f l ~init = List.fold_right f l init
+
+  (** Return the set of all identifiers bound in a given named-context. *)
+  let to_vars =
+    List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty
+
+  (** [instance_from_named_context Ω] builds an instance [args] such
+      that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
+      definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
+      gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
+  let to_instance =
+    let filter = function
+      | Declaration.LocalAssum (id, _) -> Some (Constr.mkVar id)
+      | _ -> None
+    in
+    List.map_filter filter
   end
 
 module NamedList =
   struct
     module Declaration =
       struct
-	type t = Id.t list * Constr.t option * Constr.t
-	let map = Named.Declaration.map
+        type t = Id.t list * Constr.t option * Constr.t
+
+        let map_constr f (ids, copt, ty as decl) =
+          let copt' = Option.map f copt in
+          let ty' = f ty in
+          if copt == copt' && ty == ty' then decl else (ids, copt', ty')
       end
+
     type t = Declaration.t list
+
     let fold f l ~init = List.fold_right f l init
   end
 
diff --git a/kernel/context.mli b/kernel/context.mli
index 1976e46d33..b5f3904d22 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -26,21 +26,32 @@ open Names
     Individual declarations are then designated by de Bruijn indexes. *)
 module Rel :
 sig
-  (** Representation of {e local declarations}.
-
-      [(name, None, typ)] represents a {e local assumption}.
-
-      [(name, Some value, typ)] represents a {e local definition}.
-   *)
   module Declaration :
   sig
-    type t = Name.t * Constr.t option * Constr.t
+    (* local declaration *)
+    type t = LocalAssum of Name.t * Constr.t            (** name, type *)
+           | LocalDef of Name.t * Constr.t * Constr.t   (** name, value, type *)
 
-    (** Map all terms in a given declaration. *)
-    val map : (Constr.t -> Constr.t) -> t -> t
+    (** Return the name bound by a given declaration. *)
+    val get_name : t -> Name.t
 
-    (** Reduce all terms in a given declaration to a single value. *)
-    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+    (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+    val get_value : t -> Constr.t option
+
+    (** Return the type of the name bound by a given declaration. *)
+    val get_type : t -> Constr.t
+
+    (** Set the name that is bound by a given declaration. *)
+    val set_name : Name.t -> t -> t
+
+    (** Set the type of the bound variable in a given declaration. *)
+    val set_type : Constr.t -> t -> t
+
+    (** Return [true] iff a given declaration is a local assumption. *)
+    val is_local_assum : t -> bool
+
+    (** Return [true] iff a given declaration is a local definition. *)
+    val is_local_def : t -> bool
 
     (** Check whether any term in a given declaration satisfies a given predicate. *)
     val exists : (Constr.t -> bool) -> t -> bool
@@ -50,6 +61,28 @@ sig
 
     (** Check whether the two given declarations are equal. *)
     val equal : t -> t -> bool
+
+    (** Map the name bound by a given declaration. *)
+    val map_name : (Name.t -> Name.t) -> t -> t
+
+    (** For local assumptions, this function returns the original local assumptions.
+        For local definitions, this function maps the value in the local definition. *)
+    val map_value : (Constr.t -> Constr.t) -> t -> t
+
+    (** Map the type of the name bound by a given declaration. *)
+    val map_type : (Constr.t -> Constr.t) -> t -> t
+
+    (** Map all terms in a given declaration. *)
+    val map_constr : (Constr.t -> Constr.t) -> t -> t
+
+    (** Perform a given action on all terms in a given declaration. *)
+    val iter_constr : (Constr.t -> unit) -> t -> unit
+
+    (** Reduce all terms in a given declaration to a single value. *)
+    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+
+    val to_tuple : t -> Name.t * Constr.t option * Constr.t
+    val of_tuple : Name.t * Constr.t option * Constr.t -> t
   end
 
   (** Rel-context is represented as a list of declarations.
@@ -63,6 +96,15 @@ sig
   (** Return a new rel-context enriched by with a given inner-most declaration. *)
   val add : Declaration.t -> t -> t
 
+  (** Return the number of {e local declarations} in a given context. *)
+  val length : t -> int
+
+  (** Check whether given two rel-contexts are equal. *)
+  val equal : t -> t -> bool
+
+  (** Return the number of {e local assumptions} in a given rel-context. *)
+  val nhyps : t -> int
+
   (** Return a declaration designated by a given de Bruijn index.
       @raise Not_found if the designated de Bruijn index outside the range. *)
   val lookup : int -> t -> Declaration.t
@@ -70,6 +112,9 @@ sig
   (** Map all terms in a given rel-context. *)
   val map : (Constr.t -> Constr.t) -> t -> t
 
+  (** Perform a given action on every declaration in a given rel-context. *)
+  val iter : (Constr.t -> unit) -> t -> unit
+
   (** Reduce all terms in a given rel-context to a single value.
       Innermost declarations are processed first. *)
   val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a
@@ -78,15 +123,6 @@ sig
       Outermost declarations are processed first. *)
   val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
 
-  (** Perform a given action on every declaration in a given rel-context. *)
-  val iter : (Constr.t -> unit) -> t -> unit
-
-  (** Return the number of {e local declarations} in a given context. *)
-  val length : t -> int
-
-  (** Return the number of {e local assumptions} in a given rel-context. *)
-  val nhyps : t -> int
-
   (** Map a given rel-context to a list where each {e local assumption} is mapped to [true]
       and each {e local definition} is mapped to [false]. *)
   val to_tags : t -> bool list
@@ -104,21 +140,32 @@ end
     Individual declarations are then designated by the identifiers they bind. *)
 module Named :
 sig
-  (** Representation of {e local declarations}.
-
-      [(id, None, typ)] represents a {e local assumption}.
-
-      [(id, Some value, typ)] represents a {e local definition}.
-   *)
+  (** Representation of {e local declarations}. *)
   module Declaration :
   sig
-    type t = Id.t * Constr.t option * Constr.t
+    type t = LocalAssum of Id.t * Constr.t            (** identifier, type *)
+           | LocalDef of Id.t * Constr.t * Constr.t   (** identifier, value, type *)
 
-    (** Map all terms in a given declaration. *)
-    val map : (Constr.t -> Constr.t) -> t -> t
+    (** Return the identifier bound by a given declaration. *)
+    val get_id : t -> Id.t
 
-    (** Reduce all terms in a given declaration to a single value. *)
-    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+    (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+    val get_value : t -> Constr.t option
+
+    (** Return the type of the name bound by a given declaration. *)
+    val get_type : t -> Constr.t
+
+    (** Set the identifier that is bound by a given declaration. *)
+    val set_id : Id.t -> t -> t
+
+    (** Set the type of the bound variable in a given declaration. *)
+    val set_type : Constr.t -> t -> t
+
+    (** Return [true] iff a given declaration is a local assumption. *)
+    val is_local_assum : t -> bool
+
+    (** Return [true] iff a given declaration is a local definition. *)
+    val is_local_def : t -> bool
 
     (** Check whether any term in a given declaration satisfies a given predicate. *)
     val exists : (Constr.t -> bool) -> t -> bool
@@ -128,6 +175,28 @@ sig
 
     (** Check whether the two given declarations are equal. *)
     val equal : t -> t -> bool
+
+    (** Map the identifier bound by a given declaration. *)
+    val map_id : (Id.t -> Id.t) -> t -> t
+
+    (** For local assumptions, this function returns the original local assumptions.
+        For local definitions, this function maps the value in the local definition. *)
+    val map_value : (Constr.t -> Constr.t) -> t -> t
+
+    (** Map the type of the name bound by a given declaration. *)
+    val map_type : (Constr.t -> Constr.t) -> t -> t
+
+    (** Map all terms in a given declaration. *)
+    val map_constr : (Constr.t -> Constr.t) -> t -> t
+
+    (** Perform a given action on all terms in a given declaration. *)
+    val iter_constr : (Constr.t -> unit) -> t -> unit
+
+    (** Reduce all terms in a given declaration to a single value. *)
+    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+
+    val to_tuple : t -> Id.t * Constr.t option * Constr.t
+    val of_tuple : Id.t * Constr.t option * Constr.t -> t
   end
 
   (** Rel-context is represented as a list of declarations.
@@ -141,13 +210,22 @@ sig
   (** Return a new rel-context enriched by with a given inner-most declaration. *)
   val add : Declaration.t -> t -> t
 
+  (** Return the number of {e local declarations} in a given named-context. *)
+  val length : t -> int
+
   (** Return a declaration designated by an identifier of the variable bound in that declaration.
       @raise Not_found if the designated identifier is not bound in a given named-context. *)
   val lookup : Id.t -> t -> Declaration.t
 
+  (** Check whether given two rel-contexts are equal. *)
+  val equal : t -> t -> bool
+
   (** Map all terms in a given named-context. *)
   val map : (Constr.t -> Constr.t) -> t -> t
 
+  (** Perform a given action on every declaration in a given named-context. *)
+  val iter : (Constr.t -> unit) -> t -> unit
+
   (** Reduce all terms in a given named-context to a single value.
       Innermost declarations are processed first. *)
   val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a
@@ -156,15 +234,6 @@ sig
       Outermost declarations are processed first. *)
   val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
 
-  (** Perform a given action on every declaration in a given named-context. *)
-  val iter : (Constr.t -> unit) -> t -> unit
-
-  (** Return the number of {e local declarations} in a given named-context. *)
-  val length : t -> int
-
-  (** Check whether given two named-contexts are equal. *)
-  val equal : t -> t -> bool
-
   (** Return the set of all identifiers bound in a given named-context. *)
   val to_vars : t -> Id.Set.t
 
@@ -180,7 +249,7 @@ sig
   module Declaration :
   sig
     type t = Id.t list * Constr.t option * Constr.t
-    val map : (Constr.t -> Constr.t) -> t -> t
+    val map_constr : (Constr.t -> Constr.t) -> t -> t
   end
 
   type t = Declaration.t list
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 3ab6983d8a..86d786b09a 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -201,8 +201,10 @@ let cook_constant env { from = cb; info } =
     cb.const_body
   in
   let const_hyps =
-    Context.Named.fold_outside (fun (h,_,_) hyps ->
-      List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps)
+    Context.Named.fold_outside (fun decl hyps ->
+      let open Context.Named.Declaration in
+      List.filter (fun decl' -> not (Id.equal (get_id decl) (get_id decl')))
+		  hyps)
       hyps ~init:cb.const_hyps in
   let typ = match cb.const_type with
     | RegularArity t ->
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 8f60216afa..9d58f66154 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -189,16 +189,18 @@ and slot_for_fv env fv =
       let nv = Pre_env.lookup_named_val id env in
       begin match force_lazy_val nv with
       | None ->
-          let _, b, _ = Context.Named.lookup id env.env_named_context in
-          fill_fv_cache nv id val_of_named idfun b
+         let open Context.Named in
+         let open Declaration in
+	 env.env_named_context |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun
       | Some (v, _) -> v
       end
   | FVrel i ->
       let rv = Pre_env.lookup_rel_val i env in
       begin match force_lazy_val rv with
       | None ->
-          let _, b, _ = Context.Rel.lookup i env.env_rel_context in
-          fill_fv_cache rv i val_of_rel env_of_rel b
+         let open Context.Rel in
+         let open Declaration in
+	 env.env_rel_context |> lookup i |> get_value |> fill_fv_cache rv i val_of_rel env_of_rel
       | Some (v, _) -> v
       end
   | FVuniv_var idu ->
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index f73eea030f..a09a8b7862 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -9,6 +9,7 @@
 open Declarations
 open Mod_subst
 open Util
+open Context.Rel.Declaration
 
 (** Operations concernings types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -87,10 +88,8 @@ let is_opaque cb = match cb.const_body with
 
 (** {7 Constant substitutions } *)
 
-let subst_rel_declaration sub (id,copt,t as x) =
-  let copt' = Option.smartmap (subst_mps sub) copt in
-  let t' = subst_mps sub t in
-  if copt == copt' && t == t' then x else (id,copt',t')
+let subst_rel_declaration sub =
+  map_constr (subst_mps sub)
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
@@ -140,11 +139,8 @@ let subst_const_body sub cb =
     share internal fields (e.g. constr), and not the records
     themselves. But would it really bring substantial gains ? *)
 
-let hcons_rel_decl ((n,oc,t) as d) =
-  let n' = Names.Name.hcons n
-  and oc' = Option.smartmap Term.hcons_constr oc
-  and t' = Term.hcons_types t
-  in if n' == n && oc' == oc && t' == t then d else (n',oc',t')
+let hcons_rel_decl =
+  map_type Term.hcons_types % map_value Term.hcons_constr % map_name Names.Name.hcons
 
 let hcons_rel_context l = List.smartmap hcons_rel_decl l
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index b2a77dd950..3ecfcca64c 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -18,8 +18,8 @@ open Term
 (** {6 Local entries } *)
 
 type local_entry =
-  | LocalDef of constr
-  | LocalAssum of constr
+  | LocalDefEntry of constr
+  | LocalAssumEntry of constr
 
 
 (** {6 Declaration of inductive types. } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 847e1d08f9..d8493d9baf 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -27,6 +27,7 @@ open Term
 open Vars
 open Declarations
 open Pre_env
+open Context.Rel.Declaration
 
 (* The type of environments. *)
 
@@ -72,9 +73,7 @@ let lookup_rel n env =
   Context.Rel.lookup n env.env_rel_context
 
 let evaluable_rel n env =
-  match lookup_rel n env with
-  | (_,Some _,_) -> true
-  | _ -> false
+  is_local_def (lookup_rel n env)
 
 let nb_rel env = env.env_nb_rel
 
@@ -83,7 +82,7 @@ let push_rel = push_rel
 let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x
 
 let push_rec_types (lna,typarray,_) env =
-  let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
+  let ctxt = Array.map2_i (fun i na t -> LocalAssum (na, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
 let fold_rel_context f env ~init =
@@ -107,17 +106,8 @@ let named_vals_of_val = snd
 (* [map_named_val f ctxt] apply [f] to the body and the type of
    each declarations.
    *** /!\ ***   [f t] should be convertible with t *)
-let map_named_val f (ctxt,ctxtv) =
-  let rec map ctx = match ctx with
-  | [] -> []
-  | (id, body, typ) :: rem ->
-    let body' = Option.smartmap f body in
-    let typ' = f typ in
-    let rem' = map rem in
-    if body' == body && typ' == typ && rem' == rem then ctx
-    else (id, body', typ') :: rem'
-  in
-  (map ctxt, ctxtv)
+let map_named_val f =
+  on_fst (Context.Named.map f)
 
 let empty_named_context = Context.Named.empty
 
@@ -137,11 +127,13 @@ let eq_named_context_val c1 c2 =
 
 (* A local const is evaluable if it is defined  *)
 
+open Context.Named.Declaration
+
 let named_type id env =
-  let (_,_,t) = lookup_named id env in t
+  get_type (lookup_named id env)
 
 let named_body id env =
-  let (_,b,_) = lookup_named id env in b
+  get_value (lookup_named id env)
 
 let evaluable_named id env =
   match named_body id env with
@@ -427,14 +419,14 @@ let global_vars_set env constr =
 
 let really_needed env needed =
   Context.Named.fold_inside
-    (fun need (id,copt,t) ->
-      if Id.Set.mem id need then
+    (fun need decl ->
+      if Id.Set.mem (get_id decl) need then
         let globc =
-          match copt with
-            | None -> Id.Set.empty
-            | Some c -> global_vars_set env c in
+          match decl with
+            | LocalAssum _ -> Id.Set.empty
+            | LocalDef (_,c,_) -> global_vars_set env c in
         Id.Set.union
-          (global_vars_set env t)
+          (global_vars_set env (get_type decl))
           (Id.Set.union globc need)
       else need)
     ~init:needed
@@ -443,8 +435,8 @@ let really_needed env needed =
 let keep_hyps env needed =
   let really_needed = really_needed env needed in
   Context.Named.fold_outside
-    (fun (id,_,_ as d) nsign ->
-      if Id.Set.mem id really_needed then Context.Named.add d nsign
+    (fun d nsign ->
+      if Id.Set.mem (get_id d) really_needed then Context.Named.add d nsign
       else nsign)
     (named_context env)
     ~init:empty_named_context
@@ -496,9 +488,9 @@ exception Hyp_not_found
 let apply_to_hyp (ctxt,vals) id f =
   let rec aux rtail ctxt vals =
     match ctxt, vals with
-    | (idc,c,ct as d)::ctxt, v::vals ->
-	if Id.equal idc id then
-	  (f ctxt d rtail)::ctxt, v::vals
+    | d::ctxt, v::vals ->
+	if Id.equal (get_id d) id then
+          (f ctxt d rtail)::ctxt, v::vals
 	else
 	  let ctxt',vals' = aux (d::rtail) ctxt vals in
 	  d::ctxt', v::vals'
@@ -509,8 +501,8 @@ let apply_to_hyp (ctxt,vals) id f =
 let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
   let rec aux ctxt vals =
     match ctxt,vals with
-    | (idc,c,ct as d)::ctxt, v::vals ->
-	if Id.equal idc id then
+    | d::ctxt, v::vals ->
+	if Id.equal (get_id d) id then
 	  let sign = ctxt,vals in
 	  push_named_context_val (f d sign) sign
 	else
@@ -523,8 +515,8 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
 let insert_after_hyp (ctxt,vals) id d check =
   let rec aux ctxt vals =
     match  ctxt, vals with
-    | (idc,c,ct)::ctxt', v::vals' ->
-	if Id.equal idc id then begin
+    | decl::ctxt', v::vals' ->
+	if Id.equal (get_id decl) id then begin
 	  check ctxt;
 	  push_named_context_val d (ctxt,vals)
 	end else
@@ -540,9 +532,8 @@ let remove_hyps ids check_context check_value (ctxt, vals) =
   let rec remove_hyps ctxt vals = match ctxt, vals with
   | [], [] -> [], []
   | d :: rctxt, (nid, v) :: rvals ->
-    let (id, _, _) = d in
     let ans = remove_hyps rctxt rvals in
-    if Id.Set.mem id ids then ans
+    if Id.Set.mem (get_id d) ids then ans
     else
       let (rctxt', rvals') = ans in
       let d' = check_context d in
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index ebc1853d93..7f4ba8ecbe 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -73,8 +73,8 @@ let judge_of_type u =
 
 let judge_of_relative env n =
   try
-    let (_,_,typ) = lookup_rel n env in
-      lift n typ
+    let open Context.Rel.Declaration in
+    env |> lookup_rel n |> get_type |> lift n
   with Not_found ->
     error_unbound_rel env n
 
@@ -91,7 +91,10 @@ let judge_of_variable env id =
 (* TODO: check order? *)
 let check_hyps_inclusion env f c sign =
   Context.Named.fold_outside
-    (fun (id,_,ty1) () ->
+    (fun decl () ->
+      let open Context.Named.Declaration in
+      let id = get_id decl in
+      let ty1 = get_type decl in
       try
         let ty2 = named_type id env in
         if not (eq_constr ty2 ty1) then raise Exit
@@ -325,6 +328,7 @@ let type_fixpoint env lna lar vdef vdeft =
     Ind et Constructsi un jour cela devient des constructions
     arbitraires et non plus des variables *)
 let rec execute env cstr =
+  let open Context.Rel.Declaration in
   match kind_of_term cstr with
     (* Atomic terms *)
     | Sort (Prop c) ->
@@ -368,13 +372,13 @@ let rec execute env cstr =
 
     | Lambda (name,c1,c2) ->
       let _ = execute_is_type env c1 in
-      let env1 = push_rel (name,None,c1) env in
+      let env1 = push_rel (LocalAssum (name,c1)) env in
       let c2t = execute env1 c2 in
         judge_of_abstraction env name c1 c2t
 
     | Prod (name,c1,c2) ->
       let vars = execute_is_type env c1 in
-      let env1 = push_rel (name,None,c1) env in
+      let env1 = push_rel (LocalAssum (name,c1)) env in
       let vars' = execute_is_type env1 c2 in
 	judge_of_product env name vars vars'
 
@@ -382,7 +386,7 @@ let rec execute env cstr =
       let c1t = execute env c1 in
       let _c2s = execute_is_type env c2 in
       let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in
-      let env1 = push_rel (name,Some c1,c2) env in
+      let env1 = push_rel (LocalDef (name,c1,c2)) env in
       let c3t = execute env1 c3 in
 	subst1 c1 c3t
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a8625009ce..4834f95d15 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -20,6 +20,7 @@ open Reduction
 open Typeops
 open Entries
 open Pp
+open Context.Rel.Declaration
 
 (* Tell if indices (aka real arguments) contribute to size of inductive type *)
 (* If yes, this is compatible with the univalent model *)
@@ -122,7 +123,7 @@ let infos_and_sort env t =
       match kind_of_term t with
       | Prod (name,c1,c2) ->
         let varj = infer_type env c1 in
-	let env1 = Environ.push_rel (name,None,varj.utj_val) env in
+	let env1 = Environ.push_rel (LocalAssum (name,varj.utj_val)) env in
 	let max = Universe.sup max (univ_of_sort varj.utj_type) in
 	  aux env1 c2 max
     | _ when is_constructor_head t -> max
@@ -168,12 +169,14 @@ let infer_constructor_packet env_ar_par params lc =
 (* If indices matter *)
 let cumulate_arity_large_levels env sign =
   fst (List.fold_right
-    (fun (_,b,t as d) (lev,env) ->
-      if Option.is_empty b then
+    (fun d (lev,env) ->
+     match d with
+     | LocalAssum (_,t) ->
 	let tj = infer_type env t in
 	let u = univ_of_sort tj.utj_type in
 	  (Universe.sup u lev, push_rel d env)
-      else lev, push_rel d env)
+     | LocalDef _ ->
+	lev, push_rel d env)
     sign (Universe.type0m,env))
 
 let is_impredicative env u =
@@ -184,12 +187,12 @@ let is_impredicative env u =
    from the most recent and ignoring let-definitions) is not contributing 
    or is Some u_k if its level is u_k and is contributing. *)
 let param_ccls params =
-  let fold acc = function (_, None, p) -> 
+  let fold acc = function (LocalAssum (_, p)) ->
       (let c = strip_prod_assum p in
       match kind_of_term c with
         | Sort (Type u) -> Univ.Universe.level u
         | _ -> None) :: acc
-    | _ -> acc 
+    | LocalDef _ -> acc
   in
   List.fold_left fold [] params
 
@@ -249,7 +252,7 @@ let typecheck_inductive env mie =
 	 let full_arity = it_mkProd_or_LetIn arity params in
 	 let id = ind.mind_entry_typename in
 	 let env_ar' =
-           push_rel (Name id, None, full_arity) env_ar in
+           push_rel (LocalAssum (Name id, full_arity)) env_ar in
              (* (add_constraints cst2 env_ar) in *)
 	   (env_ar', (id,full_arity,sign @ params,expltype,deflev,inflev)::l))
       (env',[])
@@ -390,7 +393,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
   let nhyps = List.length hyps in
   let rec check k index = function
     | [] -> ()
-    | (_,Some _,_)::hyps -> check k (index+1) hyps
+    | LocalDef _ :: hyps -> check k (index+1) hyps
     | _::hyps ->
         match kind_of_term (whd_betadeltaiota env lpar.(k)) with
 	  | Rel w when Int.equal w index -> check (k-1) (index+1) hyps
@@ -412,7 +415,7 @@ if Int.equal nmr 0 then 0 else
       function
 	  ([],_) -> nmr
 	| (_,[]) -> assert false (* |hyps|>=nmr *)
-	| (lp,(_,Some _,_)::hyps) -> find k (index-1) (lp,hyps)
+	| (lp, LocalDef _ :: hyps) -> find k (index-1) (lp,hyps)
 	| (p::lp,_::hyps) ->
        ( match kind_of_term (whd_betadeltaiota env p) with
 	  | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,hyps)
@@ -426,15 +429,15 @@ if Int.equal nmr 0 then 0 else
    [lra] is the list of recursive tree of each variable
  *)
 let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
- (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
+  (push_rel (LocalAssum (x,a)) env, n+1, ntypes, (Norec,ra)::lra)
 
 let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
   let auxntyp = 1 in
   let specif = (lookup_mind_specif env mi, u) in
   let ty = type_of_inductive env specif in
   let env' =
-    push_rel (Anonymous,None,
-              hnf_prod_applist env ty lpar) env in
+    let decl = LocalAssum (Anonymous, hnf_prod_applist env ty lpar) in
+    push_rel decl env in
   let ra_env' =
     (Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
@@ -726,9 +729,9 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
     let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
       it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
   in
-  let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) =
-    match b with
-    | Some c ->
+  let projections decl (i, j, kns, pbs, subst, letsubst) =
+    match decl with
+    | LocalDef (na,c,t) ->
         (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
            to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
         let c = liftn 1 j c in
@@ -746,7 +749,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
            to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *)
         let letsubst = c2 :: letsubst in
         (i, j+1, kns, pbs, subst, letsubst)
-    | None ->
+    | LocalAssum (na,t) ->
       match na with
       | Name id ->
 	let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index dd49c4a1b7..229508ea34 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -17,6 +17,7 @@ open Declareops
 open Environ
 open Reduction
 open Type_errors
+open Context.Rel.Declaration
 
 type mind_specif = mutual_inductive_body * one_inductive_body
 
@@ -77,10 +78,10 @@ let instantiate_params full t u args sign =
     anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
   let (rem_args, subs, ty) =
     Context.Rel.fold_outside
-      (fun (_,copt,_) (largs,subs,ty) ->
-        match (copt, largs, kind_of_term ty) with
-          | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
-          | (Some b,_,LetIn(_,_,_,t))    ->
+      (fun decl (largs,subs,ty) ->
+        match (decl, largs, kind_of_term ty) with
+          | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
+          | (LocalDef (_,b,_), _, LetIn(_,_,_,t))    ->
 	     (largs, (substl subs (subst_instance_constr u b))::subs, t)
 	  | (_,[],_)                -> if full then fail() else ([], subs, ty)
 	  | _                       -> fail ())
@@ -152,7 +153,7 @@ let remember_subst u subst =
 (* Propagate the new levels in the signature *)
 let make_subst env =
   let rec make subst = function
-    | (_,Some _,_)::sign, exp, args ->
+    | LocalDef _ :: sign, exp, args ->
         make subst (sign, exp, args)
     | d::sign, None::exp, args ->
         let args = match args with _::args -> args | [] -> [] in
@@ -165,7 +166,7 @@ let make_subst env =
         (* a useless extra constraint *)
         let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
           make (cons_subst u s subst) (sign, exp, args)
-    | (na,None,t)::sign, Some u::exp, [] ->
+    | LocalAssum (na,t) :: sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
         (* substitution (when [u] is distinct from all other universes in the *)
         (* template, it is identity substitution  otherwise (ie. when u is *)
@@ -314,14 +315,14 @@ let is_correct_arity env c pj ind specif params =
   let rec srec env pt ar =
     let pt' = whd_betadeltaiota env pt in
     match kind_of_term pt', ar with
-      | Prod (na1,a1,t), (_,None,a1')::ar' ->
+      | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
           let () =
             try conv env a1 a1'
             with NotConvertible -> raise (LocalArity None) in
-          srec (push_rel (na1,None,a1) env) t ar' 
+          srec (push_rel (LocalAssum (na1,a1)) env) t ar'
       (* The last Prod domain is the type of the scrutinee *)
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
-	 let env' = push_rel (na1,None,a1) env in
+	 let env' = push_rel (LocalAssum (na1,a1)) env in
 	 let ksort = match kind_of_term (whd_betadeltaiota env' a2) with
 	 | Sort s -> family_of_sort s
 	 | _ -> raise (LocalArity None) in
@@ -330,7 +331,7 @@ let is_correct_arity env c pj ind specif params =
            try conv env a1 dep_ind
            with NotConvertible -> raise (LocalArity None) in
 	   check_allowed_sort ksort specif
-      | _, (_,Some _,_ as d)::ar' ->
+      | _, (LocalDef _ as d)::ar' ->
 	  srec (push_rel d env) (lift 1 pt') ar'
       | _ ->
 	  raise (LocalArity None)
@@ -482,7 +483,7 @@ let make_renv env recarg tree =
     genv = [Lazy.lazy_from_val(Subterm(Large,tree))] }
 
 let push_var renv (x,ty,spec) =
-  { env = push_rel (x,None,ty) renv.env;
+  { env = push_rel (LocalAssum (x,ty)) renv.env;
     rel_min = renv.rel_min+1;
     genv = spec:: renv.genv }
 
@@ -568,14 +569,14 @@ let check_inductive_codomain env p =
 (* The following functions are almost duplicated from indtypes.ml, except
 that they carry here a poorer environment (containing less information). *)
 let ienv_push_var (env, lra) (x,a,ra) =
-  (push_rel (x,None,a) env, (Norec,ra)::lra)
+  (push_rel (LocalAssum (x,a)) env, (Norec,ra)::lra)
 
 let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
   let mib = Environ.lookup_mind mind env in
   let ntypes = mib.mind_ntypes in
   let push_ind specif env =
-     push_rel (Anonymous,None,
-		hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) env
+    let decl = LocalAssum (Anonymous, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in
+    push_rel decl env
   in
   let env = Array.fold_right push_ind mib.mind_packets env in
   let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in
@@ -848,7 +849,7 @@ let filter_stack_domain env ci p stack =
     let t = whd_betadeltaiota env ar in
     match stack, kind_of_term t with
     | elt :: stack', Prod (n,a,c0) ->
-      let d = (n,None,a) in
+      let d = LocalAssum (n,a) in
       let ty, args = decompose_app (whd_betadeltaiota env a) in
       let elt = match kind_of_term ty with
       | Ind ind -> 
@@ -905,10 +906,10 @@ let check_one_fix renv recpos trees def =
               end
             else
               begin
-                match pi2 (lookup_rel p renv.env) with
-                | None ->
+                match lookup_rel p renv.env with
+                | LocalAssum _ ->
                     List.iter (check_rec_call renv []) l
-                | Some c ->
+                | LocalDef (_,c,_) ->
                     try List.iter (check_rec_call renv []) l
                     with FixGuardError _ ->
                       check_rec_call renv stack (applist(lift p c,l))
@@ -983,10 +984,11 @@ let check_one_fix renv recpos trees def =
 
         | Var id ->
             begin
-              match pi2 (lookup_named id renv.env) with
-              | None ->
+              let open Context.Named.Declaration in
+              match lookup_named id renv.env with
+              | LocalAssum _ ->
                   List.iter (check_rec_call renv []) l
-              | Some c ->
+              | LocalDef (_,c,_) ->
                   try List.iter (check_rec_call renv []) l
                   with (FixGuardError _) -> 
 		    check_rec_call renv stack (applist(c,l))
@@ -1040,7 +1042,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
       match kind_of_term (whd_betadeltaiota env def) with
         | Lambda (x,a,b) ->
 	    if noccur_with_meta n nbfix a then
-	      let env' = push_rel (x, None, a) env in
+	      let env' = push_rel (LocalAssum (x,a)) env in
               if Int.equal n (k + 1) then
                 (* get the inductive type of the fixpoint *)
                 let (mind, _) =
@@ -1090,7 +1092,7 @@ let rec codomain_is_coind env c =
   let b = whd_betadeltaiota env c in
   match kind_of_term b with
     | Prod (x,a,b) ->
-	codomain_is_coind (push_rel (x, None, a) env) b
+	codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
     | _ ->
 	(try find_coinductive env b
         with Not_found ->
@@ -1131,7 +1133,7 @@ let check_one_cofix env nbfix def deftype =
 	| Lambda (x,a,b) ->
 	    let () = assert (List.is_empty args) in
             if noccur_with_meta n nbfix a then
-              let env' = push_rel (x, None, a) env in
+              let env' = push_rel (LocalAssum (x,a)) env in
               check_rec_call env' alreadygrd (n+1) tree vlra b
             else
 	      raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 711096b2b1..dabe905dee 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1832,24 +1832,25 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
   auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named)))
 
 and compile_rel env sigma univ auxdefs n =
-  let (_,body,_) = Context.Rel.lookup n env.env_rel_context in
-  let n = Context.Rel.length env.env_rel_context - n in
-  match body with
-  | Some t ->
+  let open Context.Rel in
+  let n = length env.env_rel_context - n in
+  let open Declaration in
+  match lookup n env.env_rel_context with
+  | LocalDef (_,t,_) ->
       let code = lambda_of_constr env sigma t in
       let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in
       Glet(Grel n, code)::auxdefs
-  | None -> 
+  | LocalAssum _ ->
       Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs
 
 and compile_named env sigma univ auxdefs id =
-  let (_,body,_) = Context.Named.lookup id env.env_named_context in
-  match body with
-  | Some t ->
+  let open Context.Named.Declaration in
+  match Context.Named.lookup id env.env_named_context with
+  | LocalDef (_,t,_) ->
       let code = lambda_of_constr env sigma t in
       let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in
       Glet(Gnamed id, code)::auxdefs
-  | None -> 
+  | LocalAssum _ ->
       Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
 
 let compile_constant env sigma prefix ~interactive con cb =
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 01f59df15a..91b40be7e9 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -727,7 +727,8 @@ let optimize lam =
 let lambda_of_constr env sigma c =
   set_global_env env;
   let env = Renv.make () in
-  let ids = List.rev_map (fun (id, _, _) -> id) !global_env.env_rel_context in
+  let open Context.Rel.Declaration in
+  let ids = List.rev_map get_name !global_env.env_rel_context in
   Renv.push_rels env (Array.of_list ids);
   let lam = lambda_of_constr env sigma c in
 (*  if Flags.vm_draw_opt () then begin
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 4c1b2c5a64..99d99e6940 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -18,6 +18,7 @@ open Names
 open Univ
 open Term
 open Declarations
+open Context.Named.Declaration
 
 (* The type of environments. *)
 
@@ -124,18 +125,16 @@ let env_of_rel n env =
 (* Named context *)
 
 let push_named_context_val d (ctxt,vals) =
-  let id,_,_ = d in
   let rval = ref VKnone in
-    Context.Named.add d ctxt, (id,rval)::vals
+    Context.Named.add d ctxt, (get_id d,rval)::vals
 
 let push_named d env =
 (*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
   assert (env.env_rel_context = []); *)
-  let id,body,_ = d in
   let rval = ref VKnone in
   { env_globals = env.env_globals;
     env_named_context = Context.Named.add d env.env_named_context;
-    env_named_vals = (id, rval) :: env.env_named_vals;
+    env_named_vals = (get_id d, rval) :: env.env_named_vals;
     env_rel_context = env.env_rel_context;
     env_rel_val = env.env_rel_val;
     env_nb_rel = env.env_nb_rel;
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 40b80cc5e9..cfc286135d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -24,6 +24,7 @@ open Univ
 open Environ
 open Closure
 open Esubst
+open Context.Rel.Declaration
 
 let rec is_empty_stack = function
   [] -> true
@@ -739,7 +740,7 @@ let dest_prod env =
     let t = whd_betadeltaiota env c in
     match kind_of_term t with
       | Prod (n,a,c0) ->
-          let d = (n,None,a) in
+	  let d = LocalAssum (n,a) in
 	  decrec (push_rel d env) (Context.Rel.add d m) c0
       | _ -> m,t
   in
@@ -751,10 +752,10 @@ let dest_prod_assum env =
     let rty = whd_betadeltaiota_nolet env ty in
     match kind_of_term rty with
     | Prod (x,t,c)  ->
-        let d = (x,None,t) in
+        let d = LocalAssum (x,t) in
 	prodec_rec (push_rel d env) (Context.Rel.add d l) c
     | LetIn (x,b,t,c) ->
-        let d = (x,Some b,t) in
+        let d = LocalDef (x,b,t) in
 	prodec_rec (push_rel d env) (Context.Rel.add d l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               ->
@@ -769,10 +770,10 @@ let dest_lam_assum env =
     let rty = whd_betadeltaiota_nolet env ty in
     match kind_of_term rty with
     | Lambda (x,t,c)  ->
-        let d = (x,None,t) in
+        let d = LocalAssum (x,t) in
 	lamec_rec (push_rel d env) (Context.Rel.add d l) c
     | LetIn (x,b,t,c) ->
-        let d = (x,Some b,t) in
+        let d = LocalDef (x,b,t) in
 	lamec_rec (push_rel d env) (Context.Rel.add d l) c
     | Cast (c,_,_)    -> lamec_rec env l c
     | _               -> l,rty
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e56a6e0999..8a402322f0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -60,6 +60,7 @@
 open Util
 open Names
 open Declarations
+open Context.Named.Declaration
 
 (** {6 Safe environments }
 
@@ -362,7 +363,8 @@ let check_required current_libs needed =
     hypothesis many many times, and the check performed here would
     cost too much. *)
 
-let safe_push_named (id,_,_ as d) env =
+let safe_push_named d env =
+  let id = get_id d in
   let _ =
     try
       let _ = Environ.lookup_named id env in
@@ -383,13 +385,13 @@ let push_named_def (id,de) senv =
 	(Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o)
     | _ -> assert false in
   let senv' = push_context_set poly univs senv in
-  let env'' = safe_push_named (id,Some c,typ) senv'.env in
+  let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in
     univs, {senv' with env=env''}
 
 let push_named_assum ((id,t,poly),ctx) senv =
   let senv' = push_context_set poly ctx senv in
   let t = Term_typing.translate_local_assum senv'.env t in
-  let env'' = safe_push_named (id,None,t) senv'.env in
+  let env'' = safe_push_named (LocalAssum (id,t)) senv'.env in
     {senv' with env=env''}
 
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 9ba45f5403..4416770fe4 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -383,40 +383,46 @@ let mkNamedLambda id typ c = mkLambda (Name id, typ, subst_var id c)
 let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, subst_var id c2)
 
 (* Constructs either [(x:t)c] or [[x=b:t]c] *)
-let mkProd_or_LetIn (na,body,t) c =
-  match body with
-    | None -> mkProd (na, t, c)
-    | Some b -> mkLetIn (na, b, t, c)
-
-let mkNamedProd_or_LetIn (id,body,t) c =
-  match body with
-    | None -> mkNamedProd id t c
-    | Some b -> mkNamedLetIn id b t c
+let mkProd_or_LetIn decl c =
+  let open Context.Rel.Declaration in
+  match decl with
+  | LocalAssum (na,t) -> mkProd (na, t, c)
+  | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
+
+let mkNamedProd_or_LetIn decl c =
+  let open Context.Named.Declaration in
+  match decl with
+    | LocalAssum (id,t) -> mkNamedProd id t c
+    | LocalDef (id,b,t) -> mkNamedLetIn id b t c
 
 (* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
-let mkProd_wo_LetIn (na,body,t) c =
-  match body with
-    | None -> mkProd (na,  t, c)
-    | Some b -> subst1 b c
-
-let mkNamedProd_wo_LetIn (id,body,t) c =
-  match body with
-    | None -> mkNamedProd id t c
-    | Some b -> subst1 b (subst_var id c)
+let mkProd_wo_LetIn decl c =
+  let open Context.Rel.Declaration in
+  match decl with
+  | LocalAssum (na,t) -> mkProd (na, t, c)
+  | LocalDef (na,b,t) -> subst1 b c
+
+let mkNamedProd_wo_LetIn decl c =
+  let open Context.Named.Declaration in
+  match decl with
+    | LocalAssum (id,t) -> mkNamedProd id t c
+    | LocalDef (id,b,t) -> subst1 b (subst_var id c)
 
 (* non-dependent product t1 -> t2 *)
 let mkArrow t1 t2 = mkProd (Anonymous, t1, t2)
 
 (* Constructs either [[x:t]c] or [[x=b:t]c] *)
-let mkLambda_or_LetIn (na,body,t) c =
-  match body with
-    | None -> mkLambda (na, t, c)
-    | Some b -> mkLetIn (na, b, t, c)
-
-let mkNamedLambda_or_LetIn (id,body,t) c =
-  match body with
-    | None -> mkNamedLambda id t c
-    | Some b -> mkNamedLetIn id b t c
+let mkLambda_or_LetIn decl c =
+  let open Context.Rel.Declaration in
+  match decl with
+    | LocalAssum (na,t) -> mkLambda (na, t, c)
+    | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
+
+let mkNamedLambda_or_LetIn decl c =
+  let open Context.Named.Declaration in
+  match decl with
+    | LocalAssum (id,t) -> mkNamedLambda id t c
+    | LocalDef (id,b,t) -> mkNamedLetIn id b t c
 
 (* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *)
 let prodn n env b =
@@ -576,10 +582,11 @@ let decompose_lam_n n =
 (* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
    ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
 let decompose_prod_assum =
+  let open Context.Rel.Declaration in
   let rec prodec_rec l c =
     match kind_of_term c with
-    | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (x,None,t) l) c
-    | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (x,Some b,t) l) c
+    | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) c
+    | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c
     | Cast (c,_,_)      -> prodec_rec l c
     | _               -> l,c
   in
@@ -589,9 +596,10 @@ let decompose_prod_assum =
    ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
 let decompose_lam_assum =
   let rec lamdec_rec l c =
+    let open Context.Rel.Declaration in
     match kind_of_term c with
-    | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (x,None,t) l) c
-    | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some 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
@@ -606,11 +614,13 @@ let decompose_prod_n_assum n =
     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_of_term c with
-    | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (x,None,t) l) (n-1) c
-    | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (x,Some b,t) l) (n-1) c
-    | Cast (c,_,_)      -> prodec_rec l n c
-    | c -> error "decompose_prod_n_assum: not enough assumptions"
+    else
+      let open Context.Rel.Declaration in
+      match kind_of_term c with
+      | 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
   prodec_rec Context.Rel.empty n
 
@@ -625,11 +635,13 @@ let decompose_lam_n_assum n =
     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_of_term c with
-    | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (x,None,t) l) (n-1) c
-    | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) n c
-    | Cast (c,_,_)      -> lamdec_rec l n c
-    | c -> error "decompose_lam_n_assum: not enough abstractions"
+    else
+      let open Context.Rel.Declaration in
+      match kind_of_term c with
+      | 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
 
@@ -639,11 +651,13 @@ let decompose_lam_n_decls n =
     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_of_term c with
-    | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (x,None,t) l) (n-1) c
-    | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) (n-1) c
-    | Cast (c,_,_)      -> lamdec_rec l n c
-    | c -> error "decompose_lam_n_decls: not enough abstractions"
+    else
+      let open Context.Rel.Declaration in
+      match kind_of_term c with
+      | 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
   lamdec_rec Context.Rel.empty n
 
@@ -669,10 +683,11 @@ let strip_lam_n n t = snd (decompose_lam_n n t)
 type arity = Context.Rel.t * sorts
 
 let destArity =
+  let open Context.Rel.Declaration in
   let rec prodec_rec l c =
     match kind_of_term c with
-    | Prod (x,t,c)    -> prodec_rec ((x,None,t)::l) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t) :: l) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c
     | Cast (c,_,_)      -> prodec_rec l c
     | Sort s          -> l,s
     | _               -> anomaly ~label:"destArity" (Pp.str "not an arity")
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 979165e49c..2a3ac957fb 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -138,16 +138,17 @@ let check_signatures curmb sl =
 
 let skip_trusted_seff sl b e =
   let rec aux sl b e acc =
+    let open Context.Rel.Declaration in
     match sl, kind_of_term b with
     | (None|Some 0), _ -> b, e, acc
     | Some sl, LetIn (n,c,ty,bo) ->
        aux (Some (sl-1)) bo
-         (Environ.push_rel (n,Some c,ty) e) (`Let(n,c,ty)::acc)
+         (Environ.push_rel (LocalDef (n,c,ty)) e) (`Let(n,c,ty)::acc)
     | Some sl, App(hd,arg) ->
        begin match kind_of_term hd with
        | Lambda (n,ty,bo) ->
            aux (Some (sl-1)) bo
-             (Environ.push_rel (n,None,ty) e) (`Cut(n,ty,arg)::acc)
+             (Environ.push_rel (LocalAssum (n,ty)) e) (`Cut(n,ty,arg)::acc)
        | _ -> assert false
        end
     | _ -> assert false
@@ -251,11 +252,13 @@ let global_vars_set_constant_type env = function
       ctx ~init:Id.Set.empty
 
 let record_aux env s_ty s_bo suggested_expr =
+  let open Context.Named.Declaration in
   let in_ty = keep_hyps env s_ty in
   let v =
     String.concat " "
-      (CList.map_filter (fun (id, _,_) ->
-          if List.exists (fun (id',_,_) -> Id.equal id id') in_ty then None
+      (CList.map_filter (fun decl ->
+          let id = get_id decl in
+          if List.exists (Id.equal id % get_id) in_ty then None
           else Some (Id.to_string id))
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
@@ -264,8 +267,9 @@ let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
 let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
+  let open Context.Named.Declaration in
   let check declared inferred =
-    let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
+    let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
     if not (Id.Set.subset inferred_set declared_set) then
       let l = Id.Set.elements (Idset.diff inferred_set declared_set) in
@@ -276,12 +280,13 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
         str " used but not declared:" ++
         fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
   let sort evn l =
-    List.filter (fun (id,_,_) ->
-      List.exists (fun (id',_,_) -> Names.Id.equal id id') l)
+    List.filter (fun decl ->
+      let id = get_id decl in
+      List.exists (Names.Id.equal id % get_id) l)
     (named_context env) in
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
-    let context_ids = List.map pi1 (named_context env) in
+    let context_ids = List.map get_id (named_context env) in
     match ctx with
     | None when not (List.is_empty context_ids) -> 
         (* No declared section vars, and non-empty section context:
@@ -472,7 +477,8 @@ let translate_local_def mb env id centry =
     | Undef _ -> ()
     | Def _ -> ()
     | OpaqueDef lc ->
-       let context_ids = List.map pi1 (named_context env) in
+       let open Context.Named.Declaration in
+       let context_ids = List.map get_id (named_context env) in
        let ids_typ = global_vars_set env typ in
        let ids_def = global_vars_set env
          (Opaqueproof.force_proof (opaque_tables env) lc) in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index f31cba0a8a..0ea68e2bcc 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -18,6 +18,7 @@ open Entries
 open Reduction
 open Inductive
 open Type_errors
+open Context.Rel.Declaration
 
 let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y
 
@@ -78,7 +79,7 @@ let judge_of_type u =
 
 let judge_of_relative env n =
   try
-    let (_,_,typ) = lookup_rel n env in
+    let typ = get_type (lookup_rel n env) in
     { uj_val  = mkRel n;
       uj_type = lift n typ }
   with Not_found ->
@@ -99,17 +100,19 @@ let judge_of_variable env id =
    Order does not have to be checked assuming that all names are distinct *)
 let check_hyps_inclusion env c sign =
   Context.Named.fold_outside
-    (fun (id,b1,ty1) () ->
+    (fun d1 () ->
+      let open Context.Named.Declaration in
+      let id = get_id d1 in
       try
-        let (_,b2,ty2) = lookup_named id env in
-        conv env ty2 ty1;
-        (match b2,b1 with
-        | None, None -> ()
-        | None, Some _ ->
+        let d2 = lookup_named id env in
+        conv env (get_type d2) (get_type d1);
+        (match d2,d1 with
+        | LocalAssum _, LocalAssum _ -> ()
+        | LocalAssum _, LocalDef _ ->
             (* This is wrong, because we don't know if the body is
                needed or not for typechecking: *) ()
-        | Some _, None -> raise NotConvertible
-        | Some b2, Some b1 -> conv env b2 b1);
+        | LocalDef _, LocalAssum _ -> raise NotConvertible
+        | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1);
       with Not_found | NotConvertible | Option.Heterogeneous ->
         error_reference_variables env id c)
     sign
@@ -124,9 +127,9 @@ let extract_level env p =
   match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None
 
 let extract_context_levels env l =
-  let fold l (_, b, p) = match b with
-  | None -> extract_level env p :: l
-  | _ -> l
+  let fold l = function
+    | LocalAssum (_,p) -> extract_level env p :: l
+    | LocalDef _ -> l
   in
   List.fold_left fold [] l
 
@@ -458,13 +461,13 @@ let rec execute env cstr =
 
     | Lambda (name,c1,c2) ->
       let varj = execute_type env c1 in
-      let env1 = push_rel (name,None,varj.utj_val) env in
+      let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in
       let j' = execute env1 c2 in
         judge_of_abstraction env name varj j'
 
     | Prod (name,c1,c2) ->
       let varj = execute_type env c1 in
-      let env1 = push_rel (name,None,varj.utj_val) env in
+      let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in
       let varj' = execute_type env1 c2 in
 	judge_of_product env name varj varj'
 
@@ -472,7 +475,7 @@ let rec execute env cstr =
       let j1 = execute env c1 in
       let j2 = execute_type env c2 in
       let _ = judge_of_cast env j1 DEFAULTcast j2 in
-      let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
+      let env1 = push_rel (LocalDef (name,j1.uj_val,j2.utj_val)) env in
       let j' = execute env1 c3 in
         judge_of_letin env name j1 j2 j'
 
@@ -548,12 +551,12 @@ let infer_v env cv =
 (* Typing of several terms. *)
 
 let infer_local_decl env id = function
-  | LocalDef c ->
+  | LocalDefEntry c ->
       let j = infer env c in
-      (Name id, Some j.uj_val, j.uj_type)
-  | LocalAssum c ->
+      LocalDef (Name id, j.uj_val, j.uj_type)
+  | LocalAssumEntry c ->
       let j = infer env c in
-      (Name id, None, assumption_of_judgment env j)
+      LocalAssum (Name id, assumption_of_judgment env j)
 
 let infer_local_decls env decls =
   let rec inferec env = function
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 4554c6be17..b935ab6b91 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -8,6 +8,7 @@
 
 open Names
 open Esubst
+open Context.Rel.Declaration
 
 (*********************)
 (*     Occurring     *)
@@ -159,17 +160,17 @@ let substnl laml n c = substn_many (make_subst laml) n c
 let substl laml c = substn_many (make_subst laml) 0 c
 let subst1 lam c = substn_many [|make_substituend lam|] 0 c
 
-let substnl_decl laml k r = Context.Rel.Declaration.map (fun c -> substnl laml k c) r
-let substl_decl laml r = Context.Rel.Declaration.map (fun c -> substnl laml 0 c) r
-let subst1_decl lam r = Context.Rel.Declaration.map (fun c -> subst1 lam c) r
+let substnl_decl laml k r = map_constr (fun c -> substnl laml k c) r
+let substl_decl laml r = map_constr (fun c -> substnl laml 0 c) r
+let subst1_decl lam r = map_constr (fun c -> subst1 lam c) r
 
 (* Build a substitution from an instance, inserting missing let-ins *)
 
 let subst_of_rel_context_instance sign l =
   let rec aux subst sign l =
     match sign, l with
-    | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args'
-    | (_,Some c,_)::sign', args' ->
+    | LocalAssum _ :: sign', a::args' -> aux (a::subst) sign' args'
+    | LocalDef (_,c,_)::sign', args' ->
 	aux (substl subst c :: subst) sign' args'
     | [], [] -> subst
     | _ -> Errors.anomaly (Pp.str "Instance and signature do not match")