From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 8 Jan 2016 10:00:21 +0100
Subject: CLEANUP: kernel/context.ml{,i}

The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.

Some missing comments were added to the *.mli file.

The output of ocamldoc was checked whether it looks in a reasonable way.

"TODO: cleanup" was removed

The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)

The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)

The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)

The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})

The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.

Thrown exceptions are now documented.

Naming of formal parameters was made more consistent across different functions.

Comments of similar functions in different modules are now consistent.

Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
 It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
 we can see the comments also there and do not need to open a different file if we want to see it.)

When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)

"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)

An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
---
 kernel/context.ml       | 356 ++++++++++++++++++++++++++++++------------------
 kernel/context.mli      | 243 ++++++++++++++++++++-------------
 kernel/cooking.ml       |   6 +-
 kernel/csymtable.ml     |   5 +-
 kernel/declarations.mli |   7 +-
 kernel/declareops.ml    |   2 +-
 kernel/environ.ml       |  27 ++--
 kernel/environ.mli      |  45 +++---
 kernel/fast_typeops.ml  |   2 +-
 kernel/indtypes.ml      |  33 +++--
 kernel/indtypes.mli     |   4 +-
 kernel/inductive.ml     |  15 +-
 kernel/inductive.mli    |   9 +-
 kernel/nativecode.ml    |   9 +-
 kernel/opaqueproof.ml   |   2 +-
 kernel/opaqueproof.mli  |   2 +-
 kernel/pre_env.ml       |  17 ++-
 kernel/pre_env.mli      |  13 +-
 kernel/reduction.ml     |  17 ++-
 kernel/reduction.mli    |   7 +-
 kernel/term.ml          |  33 +++--
 kernel/term.mli         |  37 +++--
 kernel/term_typing.ml   |   5 +-
 kernel/typeops.ml       |   7 +-
 kernel/typeops.mli      |   5 +-
 kernel/vars.ml          |  11 +-
 kernel/vars.mli         |  15 +-
 27 files changed, 533 insertions(+), 401 deletions(-)

(limited to 'kernel')

diff --git a/kernel/context.ml b/kernel/context.ml
index 5923048fa4..372f16a8d5 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -15,137 +15,233 @@
 (* This file defines types and combinators regarding indexes-based and
    names-based contexts *)
 
-open Util
-open Names
-
-(***************************************************************************)
-(*     Type of assumptions                                                 *)
-(***************************************************************************)
-
-type named_declaration = Id.t * Constr.t option * Constr.t
-type named_list_declaration = Id.t list * Constr.t option * Constr.t
-type rel_declaration = Name.t * Constr.t option * Constr.t
-
-let map_named_declaration_skel f (id, (v : Constr.t option), ty) =
-  (id, Option.map f v, f ty)
-let map_named_list_declaration = map_named_declaration_skel
-let map_named_declaration = map_named_declaration_skel
-
-let map_rel_declaration = map_named_declaration
-
-let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
-let fold_rel_declaration = fold_named_declaration
-
-let exists_named_declaration f (_, v, ty) = Option.cata f false v || f ty
-let exists_rel_declaration f (_, v, ty) = Option.cata f false v || f ty
-
-let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty
-let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty
-
-let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-  Id.equal i1 i2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
-
-let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
-  Name.equal n1 n2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
-
-(***************************************************************************)
-(*     Type of local contexts (telescopes)                                 *)
-(***************************************************************************)
-
-(*s Signatures of ordered optionally named variables, intended to be
-   accessed by de Bruijn indices (to represent bound variables) *)
-
-type rel_context = rel_declaration list
-
-let empty_rel_context = []
-
-let add_rel_decl d ctxt = d::ctxt
-
-let rec lookup_rel n sign =
-  match n, sign with
-  | 1, decl :: _ -> decl
-  | n, _ :: sign -> lookup_rel (n-1) sign
-  | _, []        -> raise Not_found
-
-let rel_context_length = List.length
+(** The modules defined below represent a {e local context}
+    as defined by Chapter 4 in the Reference Manual:
 
-let rel_context_nhyps hyps =
-  let rec nhyps acc = function
-    | [] -> acc
-    | (_,None,_)::hyps -> nhyps (1+acc) hyps
-    | (_,Some _,_)::hyps -> nhyps acc hyps in
-  nhyps 0 hyps
+    A {e local context} is an ordered list of of {e local declarations}
+    of names that we call {e variables}.
 
-let rel_context_tags ctx =
-  let rec aux l = function
-  | [] -> l
-  | (_,Some _,_)::ctx -> aux (true::l) ctx
-  | (_,None,_)::ctx -> aux (false::l) ctx
-  in aux [] ctx
+    A {e local declaration} of some variable can be either:
+    - a {e local assumption}, or
+    - a {e local definition}.
+*)
 
-(*s Signatures of named hypotheses. Used for section variables and
-    goal assumptions. *)
-
-type named_context = named_declaration list
-type named_list_context = named_list_declaration list
-
-let empty_named_context = []
-
-let add_named_decl d sign = d::sign
-
-let rec lookup_named id = function
-  | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
-  | _ :: sign -> lookup_named id sign
-  | [] -> raise Not_found
-
-let named_context_length = List.length
-let named_context_equal = List.equal eq_named_declaration
-
-let vars_of_named_context ctx =
-  List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty ctx
-
-let instance_from_named_context sign =
-  let filter = function
-  | (id, None, _) -> Some (Constr.mkVar id)
-  | (_, Some _, _) -> None
-  in
-  List.map_filter filter sign
-
-(** [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 extended_rel_list n hyps =
-  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 hyps
-
-let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
-
-let fold_named_context f l ~init = List.fold_right f l init
-let fold_named_list_context f l ~init = List.fold_right f l init
-let fold_named_context_reverse f ~init l = List.fold_left f init l
-
-(*s Signatures of ordered section variables *)
-type section_context = named_context
-
-let fold_rel_context f l ~init:x = List.fold_right f l x
-let fold_rel_context_reverse f ~init:x l = List.fold_left f x l
-
-let map_context f l =
-  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 l
-
-let map_rel_context = map_context
-let map_named_context = map_context
+open Util
+open Names
 
-let iter_rel_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
-let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
+(** 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}.
+
+        [(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)
+  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}.
+
+        [(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
+
+    (** 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
+  end
+
+module NamedList =
+  struct
+    module Declaration =
+      struct
+	type t = Id.t list * Constr.t option * Constr.t
+	let map = Named.Declaration.map
+      end
+    type t = Declaration.t list
+    let fold f l ~init = List.fold_right f l init
+  end
+
+type section_context = Named.t
diff --git a/kernel/context.mli b/kernel/context.mli
index 7354677474..0db82beb57 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -6,131 +6,186 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** The modules defined below represent a {e local context}
+    as defined by Chapter 4 in the Reference Manual:
+
+    A {e local context} is an ordered list of of {e local declarations}
+    of names that we call {e variables}.
+
+    A {e local declaration} of some variable can be either:
+    - a {e local assumption}, or
+    - a {e local definition}.
+
+    {e Local assumptions} are denoted in the Reference Manual as [(name : typ)] and
+    {e local definitions} are there denoted as [(name := value : typ)].
+*)
+
 open Names
 
-(** TODO: cleanup *)
+(** Representation of contexts that can capture anonymous as well as non-anonymous variables.
+    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
+
+    (** Map all terms in a given declaration. *)
+    val map : (Constr.t -> Constr.t) -> t -> t
+
+    (** Reduce all terms in a given declaration to a single value. *)
+    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+
+    (** Check whether any term in a given declaration satisfies a given predicate. *)
+    val exists : (Constr.t -> bool) -> t -> bool
+
+    (** Check whether all terms in a given declaration satisfy a given predicate. *)
+    val for_all : (Constr.t -> bool) -> t -> bool
+
+    (** Check whether the two given declarations are equal. *)
+    val equal : t -> t -> bool
+  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 *)
+  val empty : t
+
+  (** Return a new rel-context enriched by with a given inner-most declaration. *)
+  val add : Declaration.t -> t -> t
+
+  (** 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
+
+  (** Map all terms in a given rel-context. *)
+  val map : (Constr.t -> Constr.t) -> t -> t
 
-(** {6 Declarations} *)
-(** A {e declaration} has the form [(name,body,type)]. It is either an
-    {e assumption} if [body=None] or a {e definition} if
-    [body=Some actualbody]. It is referred by {e name} if [na] is an
-    identifier or by {e relative index} if [na] is not an identifier
-    (in the latter case, [na] is of type [name] but just for printing
-    purpose) *)
+  (** 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
 
-type named_declaration = Id.t * Constr.t option * Constr.t
-type named_list_declaration = Id.t list * Constr.t option * Constr.t
-type rel_declaration = Name.t * Constr.t option * Constr.t
+  (** Reduce all terms in a given rel-context to a single value.
+      Outermost declarations are processed first. *)
+  val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
 
-val map_named_declaration :
-  (Constr.t -> Constr.t) -> named_declaration -> named_declaration
-val map_named_list_declaration :
-  (Constr.t -> Constr.t) -> named_list_declaration -> named_list_declaration
-val map_rel_declaration :
-  (Constr.t -> Constr.t) -> rel_declaration -> rel_declaration
+  (** Perform a given action on every declaration in a given rel-context. *)
+  val iter : (Constr.t -> unit) -> t -> unit
 
-val fold_named_declaration :
-  (Constr.t -> 'a -> 'a) -> named_declaration -> 'a -> 'a
-val fold_rel_declaration :
-  (Constr.t -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
+  (** Return the number of {e local declarations} in a given context. *)
+  val length : t -> int
 
-val exists_named_declaration :
-  (Constr.t -> bool) -> named_declaration -> bool
-val exists_rel_declaration :
-  (Constr.t -> bool) -> rel_declaration -> bool
+  (** Return the number of {e local assumptions} in a given rel-context. *)
+  val nhyps : t -> int
 
-val for_all_named_declaration :
-  (Constr.t -> bool) -> named_declaration -> bool
-val for_all_rel_declaration :
-  (Constr.t -> bool) -> rel_declaration -> bool
+  (** 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
 
-val eq_named_declaration :
-  named_declaration -> named_declaration -> bool
+  (** [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]. *)
+  val to_extended_list : int -> t -> Constr.t list
 
-val eq_rel_declaration :
-    rel_declaration -> rel_declaration -> bool
+  (** [extended_vect n Γ] does the same, returning instead an array. *)
+  val to_extended_vect : int -> t -> Constr.t array
+end
 
-(** {6 Signatures of ordered named declarations } *)
+(** This module represents contexts that can capture non-anonymous variables.
+    Individual declarations are then designated by the identifiers they bind. *)
+module Named :
+sig
+  (** Representation of {e local declarations}.
 
-type named_context = named_declaration list
-type section_context = named_context
-type named_list_context = named_list_declaration list
-type rel_context = rel_declaration list
-(** In [rel_context], more recent declaration is on top *)
+      [(id, None, typ)] represents a {e local assumption}.
 
-val empty_named_context : named_context
-val add_named_decl : named_declaration -> named_context -> named_context
-val vars_of_named_context : named_context -> Id.Set.t
+      [(id, Some value, typ)] represents a {e local definition}.
+   *)
+  module Declaration :
+  sig
+    type t = Id.t * Constr.t option * Constr.t
 
-val lookup_named : Id.t -> named_context -> named_declaration
+    (** Map all terms in a given declaration. *)
+    val map : (Constr.t -> Constr.t) -> t -> t
 
-(** number of declarations *)
-val named_context_length : named_context -> int
+    (** Reduce all terms in a given declaration to a single value. *)
+    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
 
-(** named context equality *)
-val named_context_equal : named_context -> named_context -> bool
+    (** Check whether any term in a given declaration satisfies a given predicate. *)
+    val exists : (Constr.t -> bool) -> t -> bool
 
-(** {6 Recurrence on [named_context]: older declarations processed first } *)
-val fold_named_context :
-  (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
+    (** Check whether all terms in a given declaration satisfy a given predicate. *)
+    val for_all : (Constr.t -> bool) -> t -> bool
 
-val fold_named_list_context :
-  (named_list_declaration -> 'a -> 'a) -> named_list_context -> init:'a -> 'a
+    (** Check whether the two given declarations are equal. *)
+    val equal : t -> t -> bool
+  end
 
-(** newer declarations first *)
-val fold_named_context_reverse :
-  ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
+  (** 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
 
-(** {6 Section-related auxiliary functions } *)
+  (** empty named-context *)
+  val empty : t
 
-(** [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. *)
-val instance_from_named_context : named_context -> Constr.t list
+  (** Return a new rel-context enriched by with a given inner-most declaration. *)
+  val add : Declaration.t -> t -> t
 
-(** [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]. *)
-val extended_rel_list : int -> rel_context -> Constr.t list
+  (** 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
 
-(** [extended_rel_vect n Γ] does the same, returning instead an array. *)
-val extended_rel_vect : int -> rel_context -> Constr.t array
+  (** Map all terms in a given named-context. *)
+  val map : (Constr.t -> Constr.t) -> t -> t
 
-(** {6 ... } *)
-(** Signatures of ordered optionally named variables, intended to be
-   accessed by de Bruijn indices *)
+  (** 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
 
-(** {6 Recurrence on [rel_context]: older declarations processed first } *)
-val fold_rel_context :
-  (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+  (** Reduce all terms in a given named-context to a single value.
+      Outermost declarations are processed first. *)
+  val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
 
-(** newer declarations first *)
-val fold_rel_context_reverse :
-  ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a
+  (** Perform a given action on every declaration in a given named-context. *)
+  val iter : (Constr.t -> unit) -> t -> unit
 
-(** {6 Map function of [rel_context] } *)
-val map_rel_context : (Constr.t -> Constr.t) -> rel_context -> rel_context
+  (** Return the number of {e local declarations} in a given named-context. *)
+  val length : t -> int
 
-(** {6 Map function of [named_context] } *)
-val map_named_context : (Constr.t -> Constr.t) -> named_context -> named_context
+  (** Check whether given two named-contexts are equal. *)
+  val equal : t -> t -> bool
 
-(** {6 Map function of [rel_context] } *)
-val iter_rel_context : (Constr.t -> unit) -> rel_context -> unit
+  (** Return the set of all identifiers bound in a given named-context. *)
+  val to_vars : t -> Id.Set.t
 
-(** {6 Map function of [named_context] } *)
-val iter_named_context : (Constr.t -> unit) -> named_context -> unit
+  (** [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. *)
+  val to_instance : t -> Constr.t list
+end
 
-(** {6 Contexts of declarations referred to by de Bruijn indices } *)
+module NamedList :
+sig
+  module Declaration :
+  sig
+    type t = Id.t list * Constr.t option * Constr.t
+    val map : (Constr.t -> Constr.t) -> t -> t
+  end
 
-val empty_rel_context : rel_context
-val add_rel_decl : rel_declaration -> rel_context -> rel_context
+  type t = Declaration.t list
 
-val lookup_rel : int -> rel_context -> rel_declaration
-(** Size of the [rel_context] including LetIns *)
-val rel_context_length : rel_context -> int
-(** Size of the [rel_context] without LetIns *)
-val rel_context_nhyps : rel_context -> int
-(** Indicates whether a LetIn or a Lambda, starting from oldest declaration *)
-val rel_context_tags : rel_context -> bool list
+  val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
+end
 
+type section_context = Named.t
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index be71bd7b41..1302e71c95 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -173,7 +173,7 @@ let expmod_constr_subst cache modlist subst c =
 let cook_constr { Opaqueproof.modlist ; abstract } c =
   let cache = RefTable.create 13 in
   let expmod = expmod_constr_subst cache modlist (pi2 abstract) in
-  let hyps = Context.map_named_context expmod (pi1 abstract) in
+  let hyps = Context.Named.map expmod (pi1 abstract) in
   abstract_constant_body (expmod c) hyps
 
 let lift_univs cb subst =
@@ -195,13 +195,13 @@ let cook_constant env { from = cb; info } =
   let abstract, usubst, abs_ctx = abstract in
   let usubst, univs = lift_univs cb usubst in
   let expmod = expmod_constr_subst cache modlist usubst in
-  let hyps = Context.map_named_context expmod abstract in
+  let hyps = Context.Named.map expmod abstract in
   let body = on_body modlist (hyps, usubst, abs_ctx)
     (fun c -> abstract_constant_body (expmod c) hyps)
     cb.const_body
   in
   let const_hyps =
-    Context.fold_named_context (fun (h,_,_) hyps ->
+    Context.Named.fold_outside (fun (h,_,_) hyps ->
       List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps)
       hyps ~init:cb.const_hyps in
   let typ = match cb.const_type with
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index aa9ef66fe3..2067eb899e 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -15,7 +15,6 @@
 open Util
 open Names
 open Term
-open Context
 open Vm
 open Cemitcodes
 open Cbytecodes
@@ -190,7 +189,7 @@ 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.lookup_named id env.env_named_context in
+          let _, b, _ = Context.Named.lookup id env.env_named_context in
           fill_fv_cache nv id val_of_named idfun b
       | Some (v, _) -> v
       end
@@ -198,7 +197,7 @@ and slot_for_fv env fv =
       let rv = Pre_env.lookup_rel_val i env in
       begin match force_lazy_val rv with
       | None ->
-          let _, b, _ = lookup_rel i env.env_rel_context in
+          let _, b, _ = Context.Rel.lookup i env.env_rel_context in
           fill_fv_cache rv i val_of_rel env_of_rel b
       | Some (v, _) -> v
       end
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index dc5c17a75b..981dfe05ef 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 
 (** This module defines the internal representation of global
    declarations. This includes global constants/axioms, mutual
@@ -38,7 +37,7 @@ type ('a, 'b) declaration_arity =
   | RegularArity of 'a
   | TemplateArity of 'b
 
-type constant_type = (types, rel_context * template_arity) declaration_arity
+type constant_type = (types, Context.Rel.t * template_arity) declaration_arity
 
 (** Inlining level of parameters at functor applications.
     None means no inlining *)
@@ -117,7 +116,7 @@ type one_inductive_body = {
 
     mind_typename : Id.t; (** Name of the type: [Ii] *)
 
-    mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
+    mind_arity_ctxt : Context.Rel.t; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
 
     mind_arity : inductive_arity; (** Arity sort and original user arity *)
 
@@ -171,7 +170,7 @@ type mutual_inductive_body = {
 
     mind_nparams_rec : int;  (** Number of recursively uniform (i.e. ordinary) parameters *)
 
-    mind_params_ctxt : rel_context;  (** The context of parameters (includes let-in declaration) *)
+    mind_params_ctxt : Context.Rel.t;  (** The context of parameters (includes let-in declaration) *)
 
     mind_polymorphic : bool; (** Is it polymorphic or not *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 73cfd01221..6239d3c8d6 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -254,7 +254,7 @@ let subst_mind_body sub mib =
     mind_nparams = mib.mind_nparams;
     mind_nparams_rec = mib.mind_nparams_rec;
     mind_params_ctxt =
-      Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt;
+      Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
     mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_polymorphic = mib.mind_polymorphic;
     mind_universes = mib.mind_universes;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 09fe64d77b..da540bb051 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -24,7 +24,6 @@ open Errors
 open Util
 open Names
 open Term
-open Context
 open Vars
 open Declarations
 open Pre_env
@@ -70,7 +69,7 @@ let empty_context env =
 
 (* Rel context *)
 let lookup_rel n env =
-  lookup_rel n env.env_rel_context
+  Context.Rel.lookup n env.env_rel_context
 
 let evaluable_rel n env =
   match lookup_rel n env with
@@ -81,7 +80,7 @@ let nb_rel env = env.env_nb_rel
 
 let push_rel = push_rel
 
-let push_rel_context ctxt x = Context.fold_rel_context push_rel ctxt ~init:x
+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
@@ -120,7 +119,7 @@ let map_named_val f (ctxt,ctxtv) =
   in
   (map ctxt, ctxtv)
 
-let empty_named_context = empty_named_context
+let empty_named_context = Context.Named.empty
 
 let push_named = push_named
 let push_named_context = List.fold_right push_named
@@ -130,11 +129,11 @@ let val_of_named_context ctxt =
   List.fold_right push_named_context_val ctxt empty_named_context_val
 
 
-let lookup_named id env = Context.lookup_named id env.env_named_context
-let lookup_named_val id (ctxt,_) = Context.lookup_named id ctxt
+let lookup_named id env = Context.Named.lookup id env.env_named_context
+let lookup_named_val id (ctxt,_) = Context.Named.lookup id ctxt
 
 let eq_named_context_val c1 c2 =
-   c1 == c2 || named_context_equal (named_context_of_val c1) (named_context_of_val c2)
+   c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2)
 
 (* A local const is evaluable if it is defined  *)
 
@@ -153,7 +152,7 @@ let reset_with_named_context (ctxt,ctxtv) env =
   { env with
     env_named_context = ctxt;
     env_named_vals = ctxtv;
-    env_rel_context = empty_rel_context;
+    env_rel_context = Context.Rel.empty;
     env_rel_val = [];
     env_nb_rel = 0 }
 
@@ -176,7 +175,7 @@ let fold_named_context f env ~init =
   in fold_right env
 
 let fold_named_context_reverse f ~init env =
-  Context.fold_named_context_reverse f ~init:init (named_context env)
+  Context.Named.fold_inside f ~init:init (named_context env)
 
 
 (* Universe constraints *)
@@ -389,11 +388,11 @@ let add_mind kn mib env =
 
 let lookup_constant_variables c env =
   let cmap = lookup_constant c env in
-  Context.vars_of_named_context cmap.const_hyps
+  Context.Named.to_vars cmap.const_hyps
 
 let lookup_inductive_variables (kn,i) env =
   let mis = lookup_mind kn env in
-  Context.vars_of_named_context mis.mind_hyps
+  Context.Named.to_vars mis.mind_hyps
 
 let lookup_constructor_variables (ind,_) env =
   lookup_inductive_variables ind env
@@ -427,7 +426,7 @@ let global_vars_set env constr =
    contained in the types of the needed variables. *)
 
 let really_needed env needed =
-  Context.fold_named_context_reverse
+  Context.Named.fold_inside
     (fun need (id,copt,t) ->
       if Id.Set.mem id need then
         let globc =
@@ -443,9 +442,9 @@ let really_needed env needed =
 
 let keep_hyps env needed =
   let really_needed = really_needed env needed in
-  Context.fold_named_context
+  Context.Named.fold_outside
     (fun (id,_,_ as d) nsign ->
-      if Id.Set.mem id really_needed then add_named_decl d nsign
+      if Id.Set.mem id really_needed then Context.Named.add d nsign
       else nsign)
     (named_context env)
     ~init:empty_named_context
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 2eab32e723..f3fe4d6aef 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Declarations
 open Univ
 
@@ -42,8 +41,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
 val empty_env : env
 
 val universes     : env -> UGraph.t
-val rel_context   : env -> rel_context
-val named_context : env -> named_context
+val rel_context   : env -> Context.Rel.t
+val named_context : env -> Context.Named.t
 val named_context_val : env -> named_context_val
 
 val opaque_tables : env -> Opaqueproof.opaquetab
@@ -60,25 +59,25 @@ val empty_context : env -> bool
 (** {5 Context of de Bruijn variables ([rel_context]) } *)
 
 val nb_rel           : env -> int
-val push_rel         : rel_declaration -> env -> env
-val push_rel_context :     rel_context -> env -> env
+val push_rel         : Context.Rel.Declaration.t -> env -> env
+val push_rel_context : Context.Rel.t -> env -> env
 val push_rec_types   : rec_declaration -> env -> env
 
 (** Looks up in the context of local vars referred by indice ([rel_context]) 
    raises [Not_found] if the index points out of the context *)
-val lookup_rel    : int -> env -> rel_declaration
+val lookup_rel    : int -> env -> Context.Rel.Declaration.t
 val evaluable_rel : int -> env -> bool
 
 (** {6 Recurrence on [rel_context] } *)
 
 val fold_rel_context :
-  (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
+  (env -> Context.Rel.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
 
 (** {5 Context of variables (section variables and goal assumptions) } *)
 
-val named_context_of_val : named_context_val -> named_context
+val named_context_of_val : named_context_val -> Context.Named.t
 val named_vals_of_val : named_context_val -> Pre_env.named_vals
-val val_of_named_context : named_context -> named_context_val
+val val_of_named_context : Context.Named.t -> named_context_val
 val empty_named_context_val : named_context_val
 
 
@@ -88,18 +87,18 @@ val empty_named_context_val : named_context_val
 val map_named_val :
    (constr -> constr) -> named_context_val -> named_context_val
 
-val push_named : named_declaration -> env -> env
-val push_named_context : named_context -> env -> env
+val push_named : Context.Named.Declaration.t -> env -> env
+val push_named_context : Context.Named.t -> env -> env
 val push_named_context_val  :
-    named_declaration -> named_context_val -> named_context_val
+    Context.Named.Declaration.t -> named_context_val -> named_context_val
 
 
 
 (** Looks up in the context of local vars referred by names ([named_context]) 
    raises [Not_found] if the Id.t is not found *)
 
-val lookup_named     : variable -> env -> named_declaration
-val lookup_named_val : variable -> named_context_val -> named_declaration
+val lookup_named     : variable -> env -> Context.Named.Declaration.t
+val lookup_named_val : variable -> named_context_val -> Context.Named.Declaration.t
 val evaluable_named  : variable -> env -> bool
 val named_type : variable -> env -> types
 val named_body : variable -> env -> constr option
@@ -107,11 +106,11 @@ val named_body : variable -> env -> constr option
 (** {6 Recurrence on [named_context]: older declarations processed first } *)
 
 val fold_named_context :
-  (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
+  (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
 
 (** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
-  ('a -> named_declaration -> 'a) -> init:'a -> env -> 'a
+  ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a
 
 (** This forgets named and rel contexts *)
 val reset_context : env -> env
@@ -228,7 +227,7 @@ val vars_of_global : env -> constr -> Id.Set.t
 val really_needed : env -> Id.Set.t -> Id.Set.t
 
 (** like [really_needed] but computes a well ordered named context *)
-val keep_hyps : env -> Id.Set.t -> section_context
+val keep_hyps : env -> Id.Set.t -> Context.section_context
 
 (** {5 Unsafe judgments. }
     We introduce here the pre-type of judgments, which is
@@ -258,22 +257,22 @@ exception Hyp_not_found
    return [tail::(f head (id,_,_) (rev tail))::head].
    the value associated to id should not change *)
 val apply_to_hyp : named_context_val -> variable ->
-  (named_context -> named_declaration -> named_context -> named_declaration) ->
+  (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) ->
     named_context_val
 
 (** [apply_to_hyp_and_dependent_on sign id f g] split [sign] into
    [tail::(id,_,_)::head] and
    return [(g tail)::(f (id,_,_))::head]. *)
 val apply_to_hyp_and_dependent_on : named_context_val -> variable ->
-  (named_declaration -> named_context_val -> named_declaration) ->
-    (named_declaration -> named_context_val -> named_declaration) ->
+  (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) ->
+    (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) ->
       named_context_val
 
 val insert_after_hyp : named_context_val -> variable ->
-  named_declaration ->
-    (named_context -> unit) -> named_context_val
+  Context.Named.Declaration.t ->
+    (Context.Named.t -> unit) -> named_context_val
 
-val remove_hyps : Id.Set.t -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
+val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
 
 
 
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index b625478f25..85c74534ef 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -90,7 +90,7 @@ let judge_of_variable env id =
    variables of the current env *)
 (* TODO: check order? *)
 let check_hyps_inclusion env f c sign =
-  Context.fold_named_context
+  Context.Named.fold_outside
     (fun (id,_,ty1) () ->
       try
         let ty2 = named_type id env in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 11df40caf3..da2d213ff1 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -12,7 +12,6 @@ open Names
 open Univ
 open Term
 open Vars
-open Context
 open Declarations
 open Declareops
 open Inductive
@@ -341,7 +340,7 @@ let typecheck_inductive env mie =
 type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
-  | LocalNotConstructor of rel_context * constr list
+  | LocalNotConstructor of Context.Rel.t * constr list
   | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
@@ -361,7 +360,7 @@ let explain_ind_err id ntyp env nbpar c err =
 	raise (InductiveError
 		 (NotEnoughArgs (env,c',mkRel (kt+nbpar))))
     | LocalNotConstructor (paramsctxt,args)->
-        let nparams = rel_context_nhyps paramsctxt in
+        let nparams = Context.Rel.nhyps paramsctxt in
 	raise (InductiveError
 		 (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams,
                                   List.length args - nparams)))
@@ -384,7 +383,7 @@ let failwith_non_pos_list n ntypes l =
 
 (* Check the inductive type is called with the expected parameters *)
 let check_correct_par (env,n,ntypes,_) hyps l largs =
-  let nparams = rel_context_nhyps hyps in
+  let nparams = Context.Rel.nhyps hyps in
   let largs = Array.of_list largs in
   if Array.length largs < nparams then
     raise (IllFormedInd (LocalNotEnoughArgs l));
@@ -465,8 +464,8 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else
     arguments (used to generate induction schemes, so a priori less
     relevant to the kernel). *)
 let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
-  let lparams = rel_context_length hyps in
-  let nmr = rel_context_nhyps hyps in
+  let lparams = Context.Rel.length hyps in
+  let nmr = Context.Rel.nhyps hyps in
   (** Positivity of one argument [c] of a constructor (i.e. the
       constructor [cn] has a type of the shape [… -> c … -> P], where,
       more generally, the arrows may be dependent). *)
@@ -617,13 +616,13 @@ let check_positivity kn env_ar params inds =
   let ntypes = Array.length inds in
   let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
   let lra_ind = Array.rev_to_list rc in
-  let lparams = rel_context_length params in
-  let nmr = rel_context_nhyps params in
+  let lparams = Context.Rel.length params in
+  let nmr = Context.Rel.nhyps params in
   let check_one i (_,lcnames,lc,(sign,_)) =
     let ra_env =
       List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
-    let nargs = rel_context_nhyps sign - nmr in
+    let nargs = Context.Rel.nhyps sign - nmr in
     check_positivity_one ienv params (kn,i) nargs lcnames lc
   in
   let irecargs_nmr = Array.mapi check_one inds in
@@ -697,7 +696,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
       matching with a parameter context. *)
   let indty, paramsletsubst =
     (* [ty] = [Ind inst] is typed in context [params] *)
-    let inst = extended_rel_vect 0 paramslet in
+    let inst = Context.Rel.to_extended_vect 0 paramslet in
     let ty = mkApp (mkIndU indu, inst) in
     (* [Ind inst] is typed in context [params-wo-let] *)
     let inst' = rel_list 0 nparamargs in
@@ -710,7 +709,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
   in
   let ci = 
     let print_info =
-      { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
+      { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
       { ci_ind     = ind;
 	ci_npar    = nparamargs;
 	ci_cstr_ndecls = mind_consnrealdecls;
@@ -783,8 +782,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let hyps = used_section_variables env inds in
-  let nparamargs = rel_context_nhyps params in
-  let nparamdecls = rel_context_length params in
+  let nparamargs = Context.Rel.nhyps params in
+  let nparamdecls = Context.Rel.length params in
   let subst, ctx = Univ.abstract_universes p ctx in
   let params = Vars.subst_univs_level_context subst params in
   let env_ar = 
@@ -799,10 +798,10 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
     let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
     let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
     let consnrealdecls =
-      Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
+      Array.map (fun (d,_) -> Context.Rel.length d - Context.Rel.length params)
 	splayed_lc in
     let consnrealargs =
-      Array.map (fun (d,_) -> rel_context_nhyps d - rel_context_nhyps params)
+      Array.map (fun (d,_) -> Context.Rel.nhyps d - Context.Rel.nhyps params)
 	splayed_lc in
     (* Elimination sorts *)
     let arkind,kelim = 
@@ -835,8 +834,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
       { mind_typename = id;
 	mind_arity = arkind;
 	mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign;
-	mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
-	mind_nrealdecls = rel_context_length ar_sign - nparamdecls;
+	mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs;
+	mind_nrealdecls = Context.Rel.length ar_sign - nparamdecls;
 	mind_kelim = kelim;
 	mind_consnames = Array.of_list cnames;
 	mind_consnrealdecls = consnrealdecls;
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 01acdce5c8..1fe47b1a50 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -42,6 +42,6 @@ val enforce_indices_matter : unit -> unit
 val is_indices_matter : unit -> bool
 
 val compute_projections : pinductive -> Id.t -> Id.t ->
-  int -> Context.rel_context -> int array -> int array -> 
-  Context.rel_context -> Context.rel_context -> 
+  int -> Context.Rel.t -> int array -> int array -> 
+  Context.Rel.t -> Context.Rel.t -> 
   (constant array * projection_body array)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 632b4daeae..f9a6e04c12 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -12,7 +12,6 @@ open Names
 open Univ
 open Term
 open Vars
-open Context
 open Declarations
 open Declareops
 open Environ
@@ -77,7 +76,7 @@ let instantiate_params full t u args sign =
   let fail () =
     anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
   let (rem_args, subs, ty) =
-    Context.fold_rel_context
+    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)
@@ -297,7 +296,7 @@ let build_dependent_inductive ind (_,mip) params =
   applist
     (mkIndU ind,
        List.map (lift mip.mind_nrealdecls) params
-       @ extended_rel_list 0 realargs)
+       @ Context.Rel.to_extended_list 0 realargs)
 
 (* This exception is local *)
 exception LocalArity of (sorts_family * sorts_family * arity_error) option
@@ -350,12 +349,12 @@ let build_branches_type (ind,u) (_,mip as specif) params p =
   let build_one_branch i cty =
     let typi = full_constructor_instantiate (ind,u,specif,params) cty in
     let (cstrsign,ccl) = decompose_prod_assum typi in
-    let nargs = rel_context_length cstrsign in
+    let nargs = Context.Rel.length cstrsign in
     let (_,allargs) = decompose_app ccl in
     let (lparams,vargs) = List.chop (inductive_params specif) allargs in
     let cargs =
       let cstr = ith_constructor_of_inductive ind (i+1) in
-      let dep_cstr = applist (mkConstructU (cstr,u),lparams@(extended_rel_list 0 cstrsign)) in
+      let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list 0 cstrsign)) in
       vargs @ [dep_cstr] in
     let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in
     it_mkProd_or_LetIn base cstrsign in
@@ -499,7 +498,7 @@ let subterm_var p renv =
   with Failure _ | Invalid_argument _ -> Not_subterm
 
 let push_ctxt_renv renv ctxt =
-  let n = rel_context_length ctxt in
+  let n = Context.Rel.length ctxt in
   { env = push_rel_context ctxt renv.env;
     rel_min = renv.rel_min+n;
     genv = iterate (fun ge -> lazy Not_subterm::ge) n renv.genv }
@@ -701,7 +700,7 @@ let restrict_spec env spec p =
   else let absctx, ar = dest_lam_assum env p in
   (* Optimization: if the predicate is not dependent, no restriction is needed
      and we avoid building the recargs tree. *)
-  if noccur_with_meta 1 (rel_context_length absctx) ar then spec
+  if noccur_with_meta 1 (Context.Rel.length absctx) ar then spec
   else
   let env = push_rel_context absctx env in
   let arctx, s = dest_prod_assum env ar in
@@ -843,7 +842,7 @@ let filter_stack_domain env ci p stack =
   let absctx, ar = dest_lam_assum env p in
   (* Optimization: if the predicate is not dependent, no restriction is needed
      and we avoid building the recargs tree. *)
-  if noccur_with_meta 1 (rel_context_length absctx) ar then stack
+  if noccur_with_meta 1 (Context.Rel.length absctx) ar then stack
   else let env = push_rel_context absctx env in
   let rec filter_stack env ar stack =
     let t = whd_betadeltaiota env ar in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 5847d25f6f..541fb8282b 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Univ
 open Declarations
 open Environ
@@ -35,7 +34,7 @@ val lookup_mind_specif : env -> inductive -> mind_specif
 (** {6 Functions to build standard types related to inductive } *)
 val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list
 
-val inductive_paramdecls : mutual_inductive_body puniverses -> rel_context
+val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t
 
 val instantiate_inductive_constraints : 
   mutual_inductive_body -> universe_instance -> constraints
@@ -86,7 +85,7 @@ val build_branches_type :
     constr list -> constr -> types array
 
 (** Return the arity of an inductive type *)
-val mind_arity : one_inductive_body -> rel_context * sorts_family
+val mind_arity : one_inductive_body -> Context.Rel.t * sorts_family
 
 val inductive_sort_family : one_inductive_body -> sorts_family
 
@@ -111,8 +110,8 @@ exception SingletonInductiveBecomesProp of Id.t
 
 val max_inductive_sort : sorts array -> universe
 
-val instantiate_universes : env -> rel_context ->
-  template_arity -> constr Lazy.t array -> rel_context * sorts
+val instantiate_universes : env -> Context.Rel.t ->
+  template_arity -> constr Lazy.t array -> Context.Rel.t * sorts
 
 (** {6 Debug} *)
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 98b2d6d2e9..dd6ef1c66e 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -8,7 +8,6 @@
 open Errors
 open Names
 open Term
-open Context
 open Declarations
 open Util
 open Nativevalues
@@ -1826,15 +1825,15 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
   in
   let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in
   let auxdefs = List.fold_right get_named_val fv_named auxdefs in
-  let lvl = rel_context_length env.env_rel_context in
+  let lvl = Context.Rel.length env.env_rel_context in
   let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in
   let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in
   let aux_name = fresh_lname Anonymous in
   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,_) = lookup_rel n env.env_rel_context in
-  let n = rel_context_length env.env_rel_context - n in
+  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 code = lambda_of_constr env sigma t in
@@ -1844,7 +1843,7 @@ and compile_rel env sigma univ auxdefs n =
       Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs
 
 and compile_named env sigma univ auxdefs id =
-  let (_,body,_) = lookup_named id env.env_named_context in
+  let (_,body,_) = Context.Named.lookup id env.env_named_context in
   match body with
   | Some t ->
       let code = lambda_of_constr env sigma t in
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index badb15b561..bfddf82864 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t } 
+  abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } 
 type proofterm = (constr * Univ.universe_context_set) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 009ff82ff5..5b743a4c72 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -48,7 +48,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t } 
+  abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } 
 
 (* The type has two caveats:
    1) cook_constr is defined after
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 615b9d49ba..9fcec11143 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -15,7 +15,6 @@
 
 open Util
 open Names
-open Context
 open Univ
 open Term
 open Declarations
@@ -66,9 +65,9 @@ type named_vals = (Id.t * lazy_val) list
 
 type env = {
   env_globals       : globals;
-  env_named_context : named_context;
+  env_named_context : Context.Named.t;
   env_named_vals    : named_vals;
-  env_rel_context   : rel_context;
+  env_rel_context   : Context.Rel.t;
   env_rel_val       : lazy_val list;
   env_nb_rel        : int;
   env_stratification : stratification;
@@ -77,7 +76,7 @@ type env = {
   indirect_pterms : Opaqueproof.opaquetab;
 }
 
-type named_context_val = named_context * named_vals
+type named_context_val = Context.Named.t * named_vals
 
 let empty_named_context_val = [],[]
 
@@ -87,9 +86,9 @@ let empty_env = {
     env_inductives = Mindmap_env.empty;
     env_modules = MPmap.empty;
     env_modtypes = MPmap.empty};
-  env_named_context = empty_named_context;
+  env_named_context = Context.Named.empty;
   env_named_vals = [];
-  env_rel_context = empty_rel_context;
+  env_rel_context = Context.Rel.empty;
   env_rel_val = [];
   env_nb_rel = 0;
   env_stratification = {
@@ -107,7 +106,7 @@ let nb_rel env = env.env_nb_rel
 let push_rel d env =
   let rval = ref VKnone in
     { env with
-      env_rel_context = add_rel_decl d env.env_rel_context;
+      env_rel_context = Context.Rel.add d env.env_rel_context;
       env_rel_val = rval :: env.env_rel_val;
       env_nb_rel = env.env_nb_rel + 1 }
 
@@ -127,7 +126,7 @@ let env_of_rel n env =
 let push_named_context_val d (ctxt,vals) =
   let id,_,_ = d in
   let rval = ref VKnone in
-    add_named_decl d ctxt, (id,rval)::vals
+    Context.Named.add d ctxt, (id,rval)::vals
 
 let push_named d env =
 (*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
@@ -135,7 +134,7 @@ let push_named d env =
   let id,body,_ = d in
   let rval = ref VKnone in
   { env_globals = env.env_globals;
-    env_named_context = Context.add_named_decl d env.env_named_context;
+    env_named_context = Context.Named.add d env.env_named_context;
     env_named_vals = (id, rval) :: env.env_named_vals;
     env_rel_context = env.env_rel_context;
     env_rel_val = env.env_rel_val;
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index b499ac0c52..9cd940a881 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Declarations
 open Univ
 
@@ -46,9 +45,9 @@ type named_vals = (Id.t * lazy_val) list
 
 type env = {
     env_globals       : globals;
-    env_named_context : named_context;
+    env_named_context : Context.Named.t;
     env_named_vals    : named_vals;
-    env_rel_context   : rel_context;
+    env_rel_context   : Context.Rel.t;
     env_rel_val       : lazy_val list;
     env_nb_rel        : int;
     env_stratification : stratification;
@@ -57,7 +56,7 @@ type env = {
     indirect_pterms : Opaqueproof.opaquetab;
 }
 
-type named_context_val = named_context * named_vals
+type named_context_val = Context.Named.t * named_vals
 
 val empty_named_context_val : named_context_val
 
@@ -66,15 +65,15 @@ val empty_env : env
 (** Rel context *)
 
 val nb_rel         : env -> int
-val push_rel       : rel_declaration -> env -> env
+val push_rel       : Context.Rel.Declaration.t -> env -> env
 val lookup_rel_val : int -> env -> lazy_val
 val env_of_rel     : int -> env -> env
 
 (** Named context *)
 
 val push_named_context_val  :
-    named_declaration -> named_context_val -> named_context_val
-val push_named       : named_declaration -> env -> env
+    Context.Named.Declaration.t -> named_context_val -> named_context_val
+val push_named       : Context.Named.Declaration.t -> env -> env
 val lookup_named_val : Id.t -> env -> lazy_val
 val env_of_named     : Id.t -> env -> env
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index bf2ee27077..78222c6b6d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -20,7 +20,6 @@ open Util
 open Names
 open Term
 open Vars
-open Context
 open Univ
 open Environ
 open Closure
@@ -741,10 +740,10 @@ let dest_prod env =
     match kind_of_term t with
       | Prod (n,a,c0) ->
           let d = (n,None,a) in
-	  decrec (push_rel d env) (add_rel_decl d m) c0
+	  decrec (push_rel d env) (Context.Rel.add d m) c0
       | _ -> m,t
   in
-  decrec env empty_rel_context
+  decrec env Context.Rel.empty
 
 (* The same but preserving lets in the context, not internal ones. *)
 let dest_prod_assum env =
@@ -753,17 +752,17 @@ let dest_prod_assum env =
     match kind_of_term rty with
     | Prod (x,t,c)  ->
         let d = (x,None,t) in
-	prodec_rec (push_rel d env) (add_rel_decl d l) c
+	prodec_rec (push_rel d env) (Context.Rel.add d l) c
     | LetIn (x,b,t,c) ->
         let d = (x,Some b,t) in
-	prodec_rec (push_rel d env) (add_rel_decl d l) c
+	prodec_rec (push_rel d env) (Context.Rel.add d l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               ->
       let rty' = whd_betadeltaiota env rty in
 	if Term.eq_constr rty' rty then l, rty
 	else prodec_rec env l rty'
   in
-  prodec_rec env empty_rel_context
+  prodec_rec env Context.Rel.empty
 
 let dest_lam_assum env =
   let rec lamec_rec env l ty =
@@ -771,14 +770,14 @@ let dest_lam_assum env =
     match kind_of_term rty with
     | Lambda (x,t,c)  ->
         let d = (x,None,t) in
-	lamec_rec (push_rel d env) (add_rel_decl d l) c
+	lamec_rec (push_rel d env) (Context.Rel.add d l) c
     | LetIn (x,b,t,c) ->
         let d = (x,Some b,t) in
-	lamec_rec (push_rel d env) (add_rel_decl d l) c
+	lamec_rec (push_rel d env) (Context.Rel.add d l) c
     | Cast (c,_,_)    -> lamec_rec env l c
     | _               -> l,rty
   in
-  lamec_rec env empty_rel_context
+  lamec_rec env Context.Rel.empty
 
 exception NotArity
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index f7a8d88c27..35daff7b59 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Term
-open Context
 open Environ
 
 (***********************************************************************
@@ -99,9 +98,9 @@ val betazeta_appvect : int -> constr -> constr array -> constr
 (***********************************************************************
   s Recognizing products and arities modulo reduction *)
 
-val dest_prod       : env -> types -> rel_context * types
-val dest_prod_assum : env -> types -> rel_context * types
-val dest_lam_assum  : env -> types -> rel_context * types
+val dest_prod       : env -> types -> Context.Rel.t * types
+val dest_prod_assum : env -> types -> Context.Rel.t * types
+val dest_lam_assum  : env -> types -> Context.Rel.t * types
 
 exception NotArity
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 455248dd52..19f4b7a234 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -10,7 +10,6 @@ open Util
 open Pp
 open Errors
 open Names
-open Context
 open Vars
 
 (**********************************************************************)
@@ -590,24 +589,24 @@ let decompose_lam_n n =
 let decompose_prod_assum =
   let rec prodec_rec l c =
     match kind_of_term c with
-    | Prod (x,t,c)    -> prodec_rec (add_rel_decl (x,None,t) l) c
-    | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c
+    | 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
     | Cast (c,_,_)      -> prodec_rec l c
     | _               -> l,c
   in
-  prodec_rec empty_rel_context
+  prodec_rec Context.Rel.empty
 
 (* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
    ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
 let decompose_lam_assum =
   let rec lamdec_rec l c =
     match kind_of_term c with
-    | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) c
-    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) c
+    | 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
     | Cast (c,_,_)      -> lamdec_rec l c
     | _               -> l,c
   in
-  lamdec_rec empty_rel_context
+  lamdec_rec Context.Rel.empty
 
 (* Given a positive integer n, decompose a product or let-in term
    of the form [forall (x1:T1)..(xi:=ci:Ti)..(xn:Tn), T] into the pair
@@ -619,12 +618,12 @@ let decompose_prod_n_assum n =
   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 (add_rel_decl (x,None,t) l) (n-1) c
-    | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+    | 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"
   in
-  prodec_rec empty_rel_context n
+  prodec_rec Context.Rel.empty n
 
 (* Given a positive integer n, decompose a lambda or let-in term [fun
    (x1:T1)..(xi:=ci:Ti)..(xn:Tn) => T] into the pair of the abstracted
@@ -638,12 +637,12 @@ let decompose_lam_n_assum n =
   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 (add_rel_decl (x,None,t) l) (n-1) c
-    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) n c
+    | 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"
   in
-  lamdec_rec empty_rel_context n
+  lamdec_rec Context.Rel.empty n
 
 (* Same, counting let-in *)
 let decompose_lam_n_decls n =
@@ -652,12 +651,12 @@ let decompose_lam_n_decls n =
   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 (add_rel_decl (x,None,t) l) (n-1) c
-    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+    | 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"
   in
-  lamdec_rec empty_rel_context n
+  lamdec_rec Context.Rel.empty n
 
 let prod_assum t = fst (decompose_prod_assum t)
 let prod_n_assum n t = fst (decompose_prod_n_assum n t)
@@ -678,7 +677,7 @@ let strip_lam_n n t = snd (decompose_lam_n n t)
    Such a term can canonically be seen as the pair of a context of types
    and of a sort *)
 
-type arity = rel_context * sorts
+type arity = Context.Rel.t * sorts
 
 let destArity =
   let rec prodec_rec l c =
diff --git a/kernel/term.mli b/kernel/term.mli
index 972a67ebed..c45e043386 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Context
 
 (** {5 Redeclaration of types from module Constr and Sorts}
 
@@ -213,14 +212,14 @@ val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
 val mkNamedProd : Id.t -> types -> types -> types
 
 (** Constructs either [(x:t)c] or [[x=b:t]c] *)
-val mkProd_or_LetIn : rel_declaration -> types -> types
-val mkProd_wo_LetIn : rel_declaration -> types -> types
-val mkNamedProd_or_LetIn : named_declaration -> types -> types
-val mkNamedProd_wo_LetIn : named_declaration -> types -> types
+val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types
+val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types
 
 (** Constructs either [[x:t]c] or [[x=b:t]c] *)
-val mkLambda_or_LetIn : rel_declaration -> constr -> constr
-val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr
+val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr
+val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr
 
 (** {5 Other term constructors. } *)
 
@@ -262,8 +261,8 @@ val to_lambda : int -> constr -> constr
    where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *)
 val to_prod : int -> constr -> constr
 
-val it_mkLambda_or_LetIn : constr -> rel_context -> constr
-val it_mkProd_or_LetIn : types -> rel_context -> types
+val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
+val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
 
 (** In [lambda_applist c args], [c] is supposed to have the form
     [λΓ.c] with [Γ] without let-in; it returns [c] with the variables
@@ -314,29 +313,29 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
 
 (** Extract the premisses and the conclusion of a term of the form
    "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *)
-val decompose_prod_assum : types -> rel_context * types
+val decompose_prod_assum : types -> Context.Rel.t * types
 
 (** Idem with lambda's *)
-val decompose_lam_assum : constr -> rel_context * constr
+val decompose_lam_assum : constr -> Context.Rel.t * constr
 
 (** Idem but extract the first [n] premisses, counting let-ins. *)
-val decompose_prod_n_assum : int -> types -> rel_context * types
+val decompose_prod_n_assum : int -> types -> Context.Rel.t * types
 
 (** Idem for lambdas, _not_ counting let-ins *)
-val decompose_lam_n_assum : int -> constr -> rel_context * constr
+val decompose_lam_n_assum : int -> constr -> Context.Rel.t * constr
 
 (** Idem, counting let-ins *)
-val decompose_lam_n_decls : int -> constr -> rel_context * constr
+val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr
 
 (** Return the premisses/parameters of a type/term (let-in included) *)
-val prod_assum : types -> rel_context
-val lam_assum : constr -> rel_context
+val prod_assum : types -> Context.Rel.t
+val lam_assum : constr -> Context.Rel.t
 
 (** Return the first n-th premisses/parameters of a type (let included and counted) *)
-val prod_n_assum : int -> types -> rel_context
+val prod_n_assum : int -> types -> Context.Rel.t
 
 (** Return the first n-th premisses/parameters of a term (let included but not counted) *)
-val lam_n_assum : int -> constr -> rel_context
+val lam_n_assum : int -> constr -> Context.Rel.t
 
 (** Remove the premisses/parameters of a type/term *)
 val strip_prod : types -> types
@@ -369,7 +368,7 @@ val under_outer_cast : (constr -> constr) -> constr -> constr
     Such a term can canonically be seen as the pair of a context of types
     and of a sort *)
 
-type arity = rel_context * sorts
+type arity = Context.Rel.t * sorts
 
 (** Build an "arity" from its canonical form *)
 val mkArity : arity -> types
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a566028d40..db50a393b5 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -16,7 +16,6 @@ open Errors
 open Util
 open Names
 open Term
-open Context
 open Declarations
 open Environ
 open Entries
@@ -246,8 +245,8 @@ let infer_declaration ~trust env kn dcl =
 let global_vars_set_constant_type env = function
   | RegularArity t -> global_vars_set env t
   | TemplateArity (ctx,_) ->
-      Context.fold_rel_context
-        (fold_rel_declaration
+      Context.Rel.fold_outside
+        (Context.Rel.Declaration.fold
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4f32fdce83..35f53b7e7c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -12,7 +12,6 @@ open Names
 open Univ
 open Term
 open Vars
-open Context
 open Declarations
 open Environ
 open Entries
@@ -99,7 +98,7 @@ 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 =
-  Context.fold_named_context
+  Context.Named.fold_outside
     (fun (id,b1,ty1) () ->
       try
         let (_,b2,ty2) = lookup_named id env in
@@ -561,6 +560,6 @@ let infer_local_decls env decls =
   | (id, d) :: l ->
       let (env, l) = inferec env l in
       let d = infer_local_decl env id d in
-	(push_rel d env, add_rel_decl d l)
-  | [] -> (env, empty_rel_context) in
+	(push_rel d env, Context.Rel.add d l)
+  | [] -> (env, Context.Rel.empty) in
   inferec env decls
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 010b2b6f03..bcaa6b63ee 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -9,7 +9,6 @@
 open Names
 open Univ
 open Term
-open Context
 open Environ
 open Entries
 open Declarations
@@ -28,7 +27,7 @@ val infer_v    : env -> constr array -> unsafe_judgment array
 val infer_type : env -> types        -> unsafe_type_judgment
 
 val infer_local_decls :
-  env -> (Id.t * local_entry) list -> (env * rel_context)
+  env -> (Id.t * local_entry) list -> (env * Context.Rel.t)
 
 (** {6 Basic operations of the typing machine. } *)
 
@@ -128,4 +127,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
   constant_type
 
 (** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> constr -> section_context -> unit
+val check_hyps_inclusion : env -> constr -> Context.section_context -> unit
diff --git a/kernel/vars.ml b/kernel/vars.ml
index a00c7036fb..53543e0436 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -8,7 +8,6 @@
 
 open Names
 open Esubst
-open Context
 
 (*********************)
 (*     Occurring     *)
@@ -160,9 +159,9 @@ 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 = map_rel_declaration (fun c -> substnl laml k c) r
-let substl_decl laml r = map_rel_declaration (fun c -> substnl laml 0 c) r
-let subst1_decl lam r = map_rel_declaration (fun c -> subst1 lam c) r
+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
 
 (* Build a substitution from an instance, inserting missing let-ins *)
 
@@ -302,7 +301,7 @@ let subst_univs_level_constr subst c =
       if !changed then c' else c
 
 let subst_univs_level_context s = 
-  map_rel_context (subst_univs_level_constr s)
+  Context.Rel.map (subst_univs_level_constr s)
       
 let subst_instance_constr subst c =
   if Univ.Instance.is_empty subst then c
@@ -343,7 +342,7 @@ let subst_instance_constr subst c =
 
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
-  else map_rel_context (fun x -> subst_instance_constr s x) ctx
+  else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
 
 type id_key = constant tableKey
 let eq_id_key x y = Names.eq_table_key Constant.equal x y
diff --git a/kernel/vars.mli b/kernel/vars.mli
index a84cf0114e..659990806d 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Constr
-open Context
 
 (** {6 Occur checks } *)
 
@@ -69,10 +68,10 @@ type substl = constr list
    as if usable in [applist] while the substitution is
    represented the other way round, i.e. ending with either [u₁] or
    [c₁], as if usable for [substl]. *)
-val subst_of_rel_context_instance : rel_context -> constr list -> substl
+val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl
 
 (** For compatibility: returns the substitution reversed *)
-val adjust_subst_to_rel_context : rel_context -> constr list -> constr list
+val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list
 
 (** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an]
     for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
@@ -92,13 +91,13 @@ val subst1 : constr -> constr -> constr
     accordingly indexes in [a₁],...,[an] and [c]. In terms of typing, if
     Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=[k], then
     Γ, Γ', [substnl_decl [a₁;...;an]] k Ω ⊢. *)
-val substnl_decl : substl -> int -> rel_declaration -> rel_declaration
+val substnl_decl : substl -> int -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
 
 (** [substl_decl σ Ω] is a short-hand for [substnl_decl σ 0 Ω] *)
-val substl_decl : substl -> rel_declaration -> rel_declaration
+val substl_decl : substl -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
 
 (** [subst1_decl a Ω] is a short-hand for [substnl_decl [a] 0 Ω] *)
-val subst1_decl : constr -> rel_declaration -> rel_declaration
+val subst1_decl : constr -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
 
 (** [replace_vars k [(id₁,c₁);...;(idn,cn)] t] substitutes [Var idj] by
     [cj] in [t]. *)
@@ -136,11 +135,11 @@ val subst_univs_constr : universe_subst -> constr -> constr
 (** Level substitutions for polymorphism. *)
 
 val subst_univs_level_constr : universe_level_subst -> constr -> constr
-val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context
+val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Context.Rel.t
 
 (** Instance substitution for polymorphism. *)
 val subst_instance_constr : universe_instance -> constr -> constr
-val subst_instance_context : universe_instance -> rel_context -> rel_context
+val subst_instance_context : universe_instance -> Context.Rel.t -> Context.Rel.t
 
 type id_key = constant tableKey
 val eq_id_key : id_key -> id_key -> bool
-- 
cgit v1.2.3