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

  Originally, rel-context was represented as:

    Context.rel_context = Names.Name.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
                  | LocalDef of Names.Name.t * Constr.t * Constr.t

  Originally, named-context was represented as:

    Context.named_context = Names.Id.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Named.t = LocalAssum of Names.Id.t * Constr.t
                    | LocalDef of Names.Id.t * Constr.t * Constr.t

Motivation:

  (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
      function which looked like this:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      Suppose that you do not know about rel-context and named-context.
      (that is the case of people who just started to read the source code)
      Merlin would tell you that the type of the value you are destructing
      by "match" is:

        'a * 'b option * Constr.t                    (* worst-case scenario *)

      or

        Named.Name.t * Constr.t option * Constr.t    (* best-case scenario (?) *)

      To me, this is akin to wearing an opaque veil.
      It is hard to figure out the meaning of the values you are looking at.
      In particular, it is hard to discover the connection between the value
      we are destructing above and the datatypes and functions defined
      in the "kernel/context.ml" file.

      In this case, the connection is there, but it is not visible
      (between the function above and the "Context" module).

      ------------------------------------------------------------------------

      Now consider, what happens when the reader see the same function
      presented in the following form:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
      to jump to the corresponding definition and learn more.

      In this case, the connection is there, and it is directly visible
      (between the function above and the "Context" module).

  (2) Also, if we already have the concepts such as:
      - local declaration
      - local assumption
      - local definition
      and we describe these notions meticulously in the Reference Manual,
      then it is a real pity not to reinforce the connection
      of the actual code with the abstract description we published.

19 files changed, 638 insertions, 336 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 9bc67b5ad..dc98cc65d 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -247,8 +247,8 @@ let info_env info = info.i_cache.i_env
 
 let rec assoc_defined id = function
 | [] -> raise Not_found
-| (_, None, _) :: ctxt -> assoc_defined id ctxt
-| (id', Some c, _) :: ctxt ->
+| Context.Named.Declaration.LocalAssum _ :: ctxt -> assoc_defined id ctxt
+| Context.Named.Declaration.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 +285,9 @@ 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 iter i = function
+    | Context.Rel.Declaration.LocalAssum _ -> ()
+    | Context.Rel.Declaration.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 3be1e8323..cc1e6f176 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -33,33 +33,122 @@ open Names
     Individual declarations are then designated by de Bruijn indexes. *)
 module Rel =
   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)].
-    *)
+    (** Representation of {e local declarations}. *)
     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)
+	(* local declaration *)
+	type t = LocalAssum of Name.t * Constr.t            (* local assumption *)
+	       | LocalDef of Name.t * Constr.t * Constr.t   (* local definition *)
+
+	(** 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 (_, v, ty) = Option.cata f false v || f ty
+	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 (_, v, ty) = Option.cata f true v && f ty
+	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 (n1, v1, ty1) (n2, v2, ty2) =
-	  Name.equal n1 n2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2
+	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.
@@ -73,6 +162,21 @@ module Rel =
     (** 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 =
@@ -81,15 +185,14 @@ module Rel =
       | 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 =
-      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
+    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. *)
@@ -99,29 +202,13 @@ module Rel =
         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
+	| 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:Γ]
@@ -129,8 +216,8 @@ module Rel =
         [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
+	| Declaration.LocalAssum _ :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
+	| Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps
 	| [] -> l
       in
       reln [] 1
@@ -143,38 +230,127 @@ module Rel =
     Individual declarations are then designated by the identifiers they bind. *)
 module Named =
   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)].
-   *)
+    (** Representation of {e local declarations}. *)
     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)
+        (** local declaration *)
+	type t = LocalAssum of Id.t * Constr.t
+               | LocalDef of Id.t * Constr.t * Constr.t
+
+        (** 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 (_, v, ty) = Option.cata f false v || f ty
+	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 (_, v, ty) = Option.cata f true v && f ty
+	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 (i1, v1, ty1) (i2, v2, ty2) =
-	  Id.equal i1 i2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2
+	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
 
+    (** 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 *)
@@ -183,22 +359,23 @@ module Named =
     (** 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
-      | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
-      | _ :: sign -> lookup id sign
-      | [] -> raise Not_found
+        @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 =
-      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
+    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. *)
@@ -208,18 +385,9 @@ module Named =
         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
+      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
@@ -227,8 +395,8 @@ module Named =
         gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
     let to_instance =
       let filter = function
-	| (id, None, _) -> Some (Constr.mkVar id)
-	| (_, Some _, _) -> None
+        | Declaration.LocalAssum (id, _) -> Some (Constr.mkVar id)
+        | _ -> None
       in
       List.map_filter filter
   end
@@ -238,9 +406,15 @@ module NamedList =
     module Declaration =
       struct
 	type t = Id.t list * Constr.t option * Constr.t
-	let map = Named.Declaration.map
+
+        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 1976e46d3..a69754cc2 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            (* local assumption *)
+	   | LocalDef of Name.t * Constr.t * Constr.t   (* local definition *)
 
-    (** 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
+           | LocalDef of Id.t * Constr.t * Constr.t
 
-    (** 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 3ab6983d8..d2106f860 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -201,8 +201,11 @@ 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
+      let h = get_id decl in
+      List.filter (fun decl -> let id = get_id decl in
+                               not (Id.equal id h)) 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 8f60216af..cfbb89f06 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 Context.Named.Declaration in
+         fill_fv_cache nv id val_of_named idfun (lookup id env.env_named_context |> get_value)
       | 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 Context.Rel.Declaration in
+	 fill_fv_cache rv i val_of_rel env_of_rel (lookup i env.env_rel_context |> get_value)
       | Some (v, _) -> v
       end
   | FVuniv_var idu ->
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index f73eea030..cb67135ad 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -87,10 +87,18 @@ 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 x =
+  let open Context.Rel.Declaration in
+  match x with
+  | LocalAssum (id,t) ->
+     let t' = subst_mps sub t in
+     if t == t' then x
+     else LocalAssum (id,t')
+  | LocalDef (id,v,t) ->
+     let v' = subst_mps sub v in
+     let t' = subst_mps sub t in
+     if v == v' && t == t' then x
+     else LocalDef (id,v',t')
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
@@ -140,11 +148,20 @@ 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 d =
+  let open Context.Rel.Declaration in
+  match d with
+  | LocalAssum (n,t) ->
+     let n' = Names.Name.hcons n
+     and t' = Term.hcons_types t in
+     if n' == n && t' == t then d
+     else LocalAssum (n',t')
+  | LocalDef (n,v,t) ->
+     let n' = Names.Name.hcons n
+     and v' = Term.hcons_constr v
+     and t' = Term.hcons_types t in
+     if n' == n && v' == v && t' == t then d
+     else LocalDef (n',v',t')
 
 let hcons_rel_context l = List.smartmap hcons_rel_decl l
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 847e1d08f..1089dff92 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -72,9 +72,8 @@ 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
+  let open Context.Rel.Declaration in
+  lookup_rel n env |> is_local_def
 
 let nb_rel env = env.env_nb_rel
 
@@ -83,7 +82,8 @@ 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 open Context.Rel.Declaration 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 +107,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
 
@@ -138,10 +129,10 @@ let eq_named_context_val c1 c2 =
 (* A local const is evaluable if it is defined  *)
 
 let named_type id env =
-  let (_,_,t) = lookup_named id env in t
+  lookup_named id env |> Context.Named.Declaration.get_type
 
 let named_body id env =
-  let (_,b,_) = lookup_named id env in b
+  lookup_named id env |> Context.Named.Declaration.get_value
 
 let evaluable_named id env =
   match named_body id env with
@@ -426,15 +417,16 @@ let global_vars_set env constr =
    contained in the types of the needed variables. *)
 
 let really_needed env needed =
+  let open Context.Named.Declaration in
   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,9 @@ 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 ->
+      let open Context.Named.Declaration in
+      if Id.Set.mem (get_id d) really_needed then Context.Named.add d nsign
       else nsign)
     (named_context env)
     ~init:empty_named_context
@@ -494,11 +487,12 @@ let compile_constant_body = Cbytegen.compile_constant_body false
 exception Hyp_not_found
 
 let apply_to_hyp (ctxt,vals) id f =
+  let open Context.Named.Declaration in
   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'
@@ -507,10 +501,11 @@ let apply_to_hyp (ctxt,vals) id f =
   in aux [] ctxt vals
 
 let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
+  let open Context.Named.Declaration in
   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
@@ -521,10 +516,11 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
   in aux ctxt vals
 
 let insert_after_hyp (ctxt,vals) id d check =
+  let open Context.Named.Declaration in
   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
@@ -537,12 +533,12 @@ let insert_after_hyp (ctxt,vals) id d check =
 
 (* To be used in Logic.clear_hyps *)
 let remove_hyps ids check_context check_value (ctxt, vals) =
+  let open Context.Named.Declaration in
   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 ebc1853d9..df95c93dc 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -73,8 +73,9 @@ 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
+    let typ = get_type (lookup_rel n env) in
+    lift n typ
   with Not_found ->
     error_unbound_rel env n
 
@@ -91,7 +92,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 +329,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 +373,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 +387,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 a8625009c..4834f95d1 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 dd49c4a1b..ca29d83f6 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 711096b2b..47274a5cd 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 decl = 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.Declaration in
+  match decl 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 01f59df15..91b40be7e 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 4c1b2c5a6..99d99e694 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 40b80cc5e..cfc286135 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 e56a6e099..8a402322f 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 9ba45f540..4416770fe 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 979165e49..2a3ac957f 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 f31cba0a8..eeb12a2b4 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -77,8 +77,9 @@ let judge_of_type u =
 (*s Type of a de Bruijn index. *)
 
 let judge_of_relative env n =
+  let open Context.Rel.Declaration in
   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 ->
@@ -98,18 +99,20 @@ let judge_of_variable env id =
    variables of the current env.
    Order does not have to be checked assuming that all names are distinct *)
 let check_hyps_inclusion env c sign =
+  let open Context.Named.Declaration in
   Context.Named.fold_outside
-    (fun (id,b1,ty1) () ->
+    (fun d1 () ->
+      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,10 @@ 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 open Context.Rel.Declaration in
+  let fold l = function
+    | LocalAssum (_,p) -> extract_level env p :: l
+    | LocalDef _ -> l
   in
   List.fold_left fold [] l
 
@@ -416,6 +420,7 @@ let type_fixpoint env lna lar vdefj =
     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) ->
@@ -458,13 +463,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 +477,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'
 
@@ -550,10 +555,10 @@ let infer_v env cv =
 let infer_local_decl env id = function
   | LocalDef c ->
       let j = infer env c in
-      (Name id, Some j.uj_val, j.uj_type)
+      Context.Rel.Declaration.LocalDef (Name id, j.uj_val, j.uj_type)
   | LocalAssum c ->
       let j = infer env c in
-      (Name id, None, assumption_of_judgment env j)
+      Context.Rel.Declaration.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 4554c6be1..b935ab6b9 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")