Introducing contexts parameterized by the inner term type.

This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.

21 files changed, 202 insertions, 183 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index ae0388003..abb284f22 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -37,9 +37,11 @@ struct
   module Declaration =
   struct
     (* local declaration *)
-    type t =
-      | LocalAssum of Name.t * Constr.t            (** name, type *)
-      | LocalDef of Name.t * Constr.t * Constr.t   (** name, value, type *)
+    type ('constr, 'types) pt =
+      | LocalAssum of Name.t * 'types            (** name, type *)
+      | LocalDef of Name.t * 'constr * 'types   (** name, value, type *)
+
+    type t = (Constr.constr, Constr.types) pt
 
     (** Return the name bound by a given declaration. *)
     let get_name = function
@@ -87,12 +89,12 @@ struct
       | LocalDef (_, v, ty) -> f v && f ty
 
     (** Check whether the two given declarations are equal. *)
-    let equal decl1 decl2 =
+    let equal eq decl1 decl2 =
       match decl1, decl2 with
       | LocalAssum (n1,ty1), LocalAssum (n2, ty2) ->
-          Name.equal n1 n2 && Constr.equal ty1 ty2
+          Name.equal n1 n2 && eq ty1 ty2
       | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) ->
-          Name.equal n1 n2 && Constr.equal v1 v2 && Constr.equal ty1 ty2
+          Name.equal n1 n2 && eq v1 v2 && eq ty1 ty2
       | _ ->
           false
 
@@ -152,6 +154,7 @@ struct
   (** 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 ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
   type t = Declaration.t list
 
   (** empty rel-context *)
@@ -166,14 +169,14 @@ struct
   (** [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 nhyps ctx =
     let open Declaration in
     let rec nhyps acc = function
       | [] -> acc
       | LocalAssum _ :: hyps -> nhyps (succ acc) hyps
       | LocalDef _ :: hyps -> nhyps acc hyps
     in
-    nhyps 0
+    nhyps 0 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. *)
@@ -184,7 +187,7 @@ struct
     | _, []        -> raise Not_found
 
   (** Check whether given two rel-contexts are equal. *)
-  let equal = List.equal Declaration.equal
+  let equal eq l = List.equal (fun c -> Declaration.equal eq c) l
 
   (** Map all terms in a given rel-context. *)
   let map f = List.smartmap (Declaration.map_constr f)
@@ -202,26 +205,26 @@ struct
 
   (** 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 to_tags l =
     let rec aux l = function
       | [] -> l
       | Declaration.LocalDef _ :: ctx -> aux (true::l) ctx
       | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx
-    in aux []
+    in aux [] l
 
   (** [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 to_extended_list mk n l =
     let rec reln l p = function
-      | Declaration.LocalAssum _ :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
+      | Declaration.LocalAssum _ :: hyps -> reln (mk (n+p) :: l) (p+1) hyps
       | Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps
       | [] -> l
     in
-    reln [] 1
+    reln [] 1 l
 
   (** [extended_vect n Γ] does the same, returning instead an array. *)
-  let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps)
+  let to_extended_vect mk n hyps = Array.of_list (to_extended_list mk n hyps)
 end
 
 (** This module represents contexts that can capture non-anonymous variables.
@@ -232,9 +235,11 @@ struct
   module Declaration =
   struct
     (** local declaration *)
-    type t =
-      | LocalAssum of Id.t * Constr.t             (** identifier, type *)
-      | LocalDef of Id.t * Constr.t * Constr.t    (** identifier, value, type *)
+    type ('constr, 'types) pt =
+      | LocalAssum of Id.t * 'types             (** identifier, type *)
+      | LocalDef of Id.t * 'constr * 'types    (** identifier, value, type *)
+
+    type t = (Constr.constr, Constr.types) pt
 
     (** Return the identifier bound by a given declaration. *)
     let get_id = function
@@ -282,12 +287,12 @@ struct
       | LocalDef (_, v, ty) -> f v && f ty
 
     (** Check whether the two given declarations are equal. *)
-    let equal decl1 decl2 =
+    let equal eq decl1 decl2 =
       match decl1, decl2 with
       | LocalAssum (id1, ty1), LocalAssum (id2, ty2) ->
-          Id.equal id1 id2 && Constr.equal ty1 ty2
+          Id.equal id1 id2 && eq ty1 ty2
       | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) ->
-          Id.equal id1 id2 && Constr.equal v1 v2 && Constr.equal ty1 ty2
+          Id.equal id1 id2 && eq v1 v2 && eq ty1 ty2
       | _ ->
           false
 
@@ -362,6 +367,7 @@ 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 ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
   type t = Declaration.t list
 
   (** empty named-context *)
@@ -380,7 +386,7 @@ struct
     | [] -> raise Not_found
 
   (** Check whether given two named-contexts are equal. *)
-  let equal = List.equal Declaration.equal
+  let equal eq l = List.equal (fun c -> Declaration.equal eq c) l
 
   (** Map all terms in a given named-context. *)
   let map f = List.smartmap (Declaration.map_constr f)
@@ -397,28 +403,30 @@ struct
   let fold_outside f l ~init = List.fold_right f l init
 
   (** Return the set of all identifiers bound in a given named-context. *)
-  let to_vars =
-    List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty
+  let to_vars l =
+    List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty l
 
   (** [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 to_instance mk l =
     let filter = function
-      | Declaration.LocalAssum (id, _) -> Some (Constr.mkVar id)
+      | Declaration.LocalAssum (id, _) -> Some (mk id)
       | _ -> None
     in
-    List.map_filter filter
+    List.map_filter filter l
 end
 
 module Compacted =
   struct
     module Declaration =
       struct
-        type t =
-          | LocalAssum of Id.t list * Constr.t
-          | LocalDef of Id.t list * Constr.t * Constr.t
+        type ('constr, 'types) pt =
+          | LocalAssum of Id.t list * 'types
+          | LocalDef of Id.t list * 'constr * 'types
+
+        type t = (Constr.constr, Constr.types) pt
 
         let map_constr f = function
           | LocalAssum (ids, ty) as decl ->
@@ -442,6 +450,7 @@ module Compacted =
              List.map (fun id -> Named.Declaration.LocalDef (id,v,t)) ids
       end
 
+    type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
     type t = Declaration.t list
 
     let fold f l ~init = List.fold_right f l init
diff --git a/kernel/context.mli b/kernel/context.mli
index 955e214cb..0c666a25d 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -29,110 +29,115 @@ sig
   module Declaration :
   sig
     (* local declaration *)
-    type t = LocalAssum of Name.t * Constr.t            (** name, type *)
-           | LocalDef of Name.t * Constr.t * Constr.t   (** name, value, type *)
+    type ('constr, 'types) pt =
+    | LocalAssum of Name.t * 'types            (** name, type *)
+    | LocalDef of Name.t * 'constr * 'types   (** name, value, type *)
+
+    type t = (Constr.constr, Constr.types) pt
 
     (** Return the name bound by a given declaration. *)
-    val get_name : t -> Name.t
+    val get_name : ('c, 't) pt -> Name.t
 
     (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
-    val get_value : t -> Constr.t option
+    val get_value : ('c, 't) pt -> 'c option
 
     (** Return the type of the name bound by a given declaration. *)
-    val get_type : t -> Constr.t
+    val get_type : ('c, 't) pt -> 't
 
     (** Set the name that is bound by a given declaration. *)
-    val set_name : Name.t -> t -> t
+    val set_name : Name.t -> ('c, 't) pt -> ('c, 't) pt
 
     (** Set the type of the bound variable in a given declaration. *)
-    val set_type : Constr.t -> t -> t
+    val set_type : 't -> ('c, 't) pt -> ('c, 't) pt
 
     (** Return [true] iff a given declaration is a local assumption. *)
-    val is_local_assum : t -> bool
+    val is_local_assum : ('c, 't) pt -> bool
 
     (** Return [true] iff a given declaration is a local definition. *)
-    val is_local_def : t -> bool
+    val is_local_def : ('c, 't) pt -> bool
 
     (** Check whether any term in a given declaration satisfies a given predicate. *)
-    val exists : (Constr.t -> bool) -> t -> bool
+    val exists : ('c -> bool) -> ('c, 'c) pt -> bool
 
     (** Check whether all terms in a given declaration satisfy a given predicate. *)
-    val for_all : (Constr.t -> bool) -> t -> bool
+    val for_all : ('c -> bool) -> ('c, 'c) pt -> bool
 
     (** Check whether the two given declarations are equal. *)
-    val equal : t -> t -> bool
+    val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool
 
     (** Map the name bound by a given declaration. *)
-    val map_name : (Name.t -> Name.t) -> t -> t
+    val map_name : (Name.t -> Name.t) -> ('c, 't) pt -> ('c, 't) pt
 
     (** 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
+    val map_value : ('c -> 'c) -> ('c, 't) pt -> ('c, 't) pt
 
     (** Map the type of the name bound by a given declaration. *)
-    val map_type : (Constr.t -> Constr.t) -> t -> t
+    val map_type : ('t -> 't) -> ('c, 't) pt -> ('c, 't) pt
 
     (** Map all terms in a given declaration. *)
-    val map_constr : (Constr.t -> Constr.t) -> t -> t
+    val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
 
     (** Perform a given action on all terms in a given declaration. *)
-    val iter_constr : (Constr.t -> unit) -> t -> unit
+    val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit
 
     (** Reduce all terms in a given declaration to a single value. *)
-    val fold_constr : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+    val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a
 
-    val to_tuple : t -> Name.t * Constr.t option * Constr.t
+    val to_tuple : ('c, 't) pt -> Name.t * 'c option * 't
   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 ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
   type t = Declaration.t list
 
   (** empty rel-context *)
-  val empty : t
+  val empty : ('c, 't) pt
 
   (** Return a new rel-context enriched by with a given inner-most declaration. *)
-  val add : Declaration.t -> t -> t
+  val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt
 
   (** Return the number of {e local declarations} in a given context. *)
-  val length : t -> int
+  val length : ('c, 't) pt -> int
 
   (** Check whether given two rel-contexts are equal. *)
-  val equal : t -> t -> bool
+  val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool
 
   (** Return the number of {e local assumptions} in a given rel-context. *)
-  val nhyps : t -> int
+  val nhyps : ('c, 't) pt -> 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
+  val lookup : int -> ('c, 't) pt -> ('c, 't) Declaration.pt
 
   (** Map all terms in a given rel-context. *)
-  val map : (Constr.t -> Constr.t) -> t -> t
+  val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
 
   (** Perform a given action on every declaration in a given rel-context. *)
-  val iter : (Constr.t -> unit) -> t -> unit
+  val iter : ('c -> unit) -> ('c, 'c) pt -> 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
+  val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a
 
   (** 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 fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a
 
   (** 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 to_tags : ('c, 't) pt -> bool list
 
-  (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+  (** [extended_list mk 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
+      [args] where [mk] is used to build the corresponding variables.
+      Example: for [x:T, y:=c, z:U] and [n]=2, it gives [mk 5, mk 3]. *)
+  val to_extended_list : (int -> 'r) -> int -> ('c, 't) pt -> 'r list
 
   (** [extended_vect n Γ] does the same, returning instead an array. *)
-  val to_extended_vect : int -> t -> Constr.t array
+  val to_extended_vect : (int -> 'r) -> int -> ('c, 't) pt -> 'r array
 end
 
 (** This module represents contexts that can capture non-anonymous variables.
@@ -142,129 +147,136 @@ sig
   (** Representation of {e local declarations}. *)
   module Declaration :
   sig
-    type t = LocalAssum of Id.t * Constr.t            (** identifier, type *)
-           | LocalDef of Id.t * Constr.t * Constr.t   (** identifier, value, type *)
+    type ('constr, 'types) pt =
+      | LocalAssum of Id.t * 'types             (** identifier, type *)
+      | LocalDef of Id.t * 'constr * 'types    (** identifier, value, type *)
+
+    type t = (Constr.constr, Constr.types) pt
 
     (** Return the identifier bound by a given declaration. *)
-    val get_id : t -> Id.t
+    val get_id : ('c, 't) pt -> Id.t
 
     (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
-    val get_value : t -> Constr.t option
+    val get_value : ('c, 't) pt -> 'c option
 
     (** Return the type of the name bound by a given declaration. *)
-    val get_type : t -> Constr.t
+    val get_type : ('c, 't) pt -> 't
 
     (** Set the identifier that is bound by a given declaration. *)
-    val set_id : Id.t -> t -> t
+    val set_id : Id.t -> ('c, 't) pt -> ('c, 't) pt
 
     (** Set the type of the bound variable in a given declaration. *)
-    val set_type : Constr.t -> t -> t
+    val set_type : 't -> ('c, 't) pt -> ('c, 't) pt
 
     (** Return [true] iff a given declaration is a local assumption. *)
-    val is_local_assum : t -> bool
+    val is_local_assum : ('c, 't) pt -> bool
 
     (** Return [true] iff a given declaration is a local definition. *)
-    val is_local_def : t -> bool
+    val is_local_def : ('c, 't) pt -> bool
 
     (** Check whether any term in a given declaration satisfies a given predicate. *)
-    val exists : (Constr.t -> bool) -> t -> bool
+    val exists : ('c -> bool) -> ('c, 'c) pt -> bool
 
     (** Check whether all terms in a given declaration satisfy a given predicate. *)
-    val for_all : (Constr.t -> bool) -> t -> bool
+    val for_all : ('c -> bool) -> ('c, 'c) pt -> bool
 
     (** Check whether the two given declarations are equal. *)
-    val equal : t -> t -> bool
+    val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool
 
     (** Map the identifier bound by a given declaration. *)
-    val map_id : (Id.t -> Id.t) -> t -> t
+    val map_id : (Id.t -> Id.t) -> ('c, 't) pt -> ('c, 't) pt
 
     (** 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
+    val map_value : ('c -> 'c) -> ('c, 't) pt -> ('c, 't) pt
 
     (** Map the type of the name bound by a given declaration. *)
-    val map_type : (Constr.t -> Constr.t) -> t -> t
+    val map_type : ('t -> 't) -> ('c, 't) pt -> ('c, 't) pt
 
     (** Map all terms in a given declaration. *)
-    val map_constr : (Constr.t -> Constr.t) -> t -> t
+    val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
 
     (** Perform a given action on all terms in a given declaration. *)
-    val iter_constr : (Constr.t -> unit) -> t -> unit
+    val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit
 
     (** Reduce all terms in a given declaration to a single value. *)
-    val fold_constr : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+    val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a
 
-    val to_tuple : t -> Id.t * Constr.t option * Constr.t
-    val of_tuple : Id.t * Constr.t option * Constr.t -> t
+    val to_tuple : ('c, 't) pt -> Id.t * 'c option * 't
+    val of_tuple : Id.t * 'c option * 't -> ('c, 't) pt
 
     (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value.
         The function provided as the first parameter determines how to translate "names" to "ids". *)
-    val of_rel_decl : (Name.t -> Id.t) -> Rel.Declaration.t -> t
+    val of_rel_decl : (Name.t -> Id.t) -> ('c, 't) Rel.Declaration.pt -> ('c, 't) pt
 
     (** Convert [Named.Declaration.t] value to the corresponding [Rel.Declaration.t] value. *)
     (* TODO: Move this function to [Rel.Declaration] module and rename it to [of_named]. *)
-    val to_rel_decl : t -> Rel.Declaration.t
+    val to_rel_decl : ('c, 't) pt -> ('c, 't) Rel.Declaration.pt
   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 ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
   type t = Declaration.t list
 
   (** empty named-context *)
-  val empty : t
+  val empty : ('c, 't) pt
 
   (** Return a new rel-context enriched by with a given inner-most declaration. *)
-  val add : Declaration.t -> t -> t
+  val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt
 
   (** Return the number of {e local declarations} in a given named-context. *)
-  val length : t -> int
+  val length : ('c, 't) pt -> 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
+  val lookup : Id.t -> ('c, 't) pt -> ('c, 't) Declaration.pt
 
   (** Check whether given two rel-contexts are equal. *)
-  val equal : t -> t -> bool
+  val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool
 
   (** Map all terms in a given named-context. *)
-  val map : (Constr.t -> Constr.t) -> t -> t
+  val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
 
   (** Perform a given action on every declaration in a given named-context. *)
-  val iter : (Constr.t -> unit) -> t -> unit
+  val iter : ('c -> unit) -> ('c, 'c) pt -> 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
+  val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> '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
+  val fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a
 
   (** Return the set of all identifiers bound in a given named-context. *)
-  val to_vars : t -> Id.Set.t
+  val to_vars : ('c, 't) pt -> Id.Set.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 to_instance : t -> Constr.t list
+  val to_instance : (Id.t -> 'r) -> ('c, 't) pt -> 'r list
 end
 
 module Compacted :
 sig
   module Declaration :
   sig
-    type t =
-      | LocalAssum of Id.t list * Constr.t
-      | LocalDef of Id.t list * Constr.t * Constr.t
+    type ('constr, 'types) pt =
+      | LocalAssum of Id.t list * 'types
+      | LocalDef of Id.t list * 'constr * 'types
+
+    type t = (Constr.constr, Constr.types) pt
 
-    val map_constr : (Constr.t -> Constr.t) -> t -> t
-    val of_named_decl : Named.Declaration.t -> t
-    val to_named_context : t -> Named.t
+    val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
+    val of_named_decl : ('c, 't) Named.Declaration.pt -> ('c, 't) pt
+    val to_named_context : ('c, 't) pt -> ('c, 't) Named.pt
   end
 
+  type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
   type t = Declaration.t list
 
-  val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
+  val fold : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a
 end
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5688813ad..9986f439a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -120,7 +120,7 @@ let lookup_named = lookup_named
 let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map)
 
 let eq_named_context_val c1 c2 =
-   c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2)
+   c1 == c2 || Context.Named.equal Constr.equal (named_context_of_val c1) (named_context_of_val c2)
 
 (* A local const is evaluable if it is defined  *)
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index de97268b3..2ff419338 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -734,7 +734,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 = Context.Rel.to_extended_vect 0 paramslet in
+    let inst = Context.Rel.to_extended_vect mkRel 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
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 3c4c2796e..d8d365c34 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -297,7 +297,7 @@ let build_dependent_inductive ind (_,mip) params =
   applist
     (mkIndU ind,
        List.map (lift mip.mind_nrealdecls) params
-       @ Context.Rel.to_extended_list 0 realargs)
+       @ Context.Rel.to_extended_list mkRel 0 realargs)
 
 (* This exception is local *)
 exception LocalArity of (sorts_family * sorts_family * arity_error) option
@@ -355,7 +355,7 @@ let build_branches_type (ind,u) (_,mip as specif) params p =
     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@(Context.Rel.to_extended_list 0 cstrsign)) in
+      let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list mkRel 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
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 519633bbe..34159d945 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -310,7 +310,7 @@ let project_hint pri l2r r =
   let p =
     if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
   let p = EConstr.of_constr p in
-  let c = Reductionops.whd_beta sigma (mkApp (c, Array.map EConstr.of_constr (Context.Rel.to_extended_vect 0 sign))) in
+  let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
   let id =
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0e4c6619b..3b5662a24 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -943,7 +943,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
   let tms = List.fold_right2 (fun par arg tomatch ->
     match EConstr.kind sigma par with
     | Rel i -> relocate_index_tomatch sigma (i+n) (destRel sigma arg) tomatch
-    | _ -> tomatch) (realargs@[cur]) (List.map EConstr.of_constr (Context.Rel.to_extended_list 0 sign))
+    | _ -> tomatch) (realargs@[cur]) (Context.Rel.to_extended_list EConstr.mkRel 0 sign)
        (lift_tomatch_stack n tms) in
   (* Pred is already dependent in the current term to match (if      *)
   (* (na<>Anonymous) and its realargs; we just need to adjust it to  *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 1adeb4db2..431d1ff16 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -63,7 +63,7 @@ let check_privacy_block mib =
 
 let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
   let lnamespar = Vars.subst_instance_context u mib.mind_params_ctxt in
-  let indf = make_ind_family(pind, Context.Rel.to_extended_list 0 lnamespar) in
+  let indf = make_ind_family(pind, Context.Rel.to_extended_list mkRel 0 lnamespar) in
   let constrs = get_constructors env indf in
   let projs = get_projections env indf in
 
@@ -93,8 +93,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
       let pbody =
         appvect
           (mkRel (ndepar + nbprod),
-           if dep then Context.Rel.to_extended_vect 0 deparsign
-           else Context.Rel.to_extended_vect 1 arsign) in
+           if dep then Context.Rel.to_extended_vect mkRel 0 deparsign
+           else Context.Rel.to_extended_vect mkRel 1 arsign) in
       let p =
 	it_mkLambda_or_LetIn_name env'
 	  ((if dep then mkLambda_name env' else mkLambda)
@@ -168,7 +168,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	    let base = applist (lift i pk,realargs) in
             if depK then
 	      Reduction.beta_appvect
-                base [|applist (mkRel (i+1), Context.Rel.to_extended_list 0 sign)|]
+                base [|applist (mkRel (i+1), Context.Rel.to_extended_list mkRel 0 sign)|]
             else
 	      base
       	| _ ->
@@ -244,7 +244,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
      	| Ind _ ->
             let realargs = List.skipn nparrec largs
-            and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect 0 hyps) in
+            and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect mkRel 0 hyps) in
             applist(lift i fk,realargs@[arg])
      	| _ ->
 	   let t' = whd_all env sigma (EConstr.of_constr p) in
@@ -323,7 +323,7 @@ let mis_make_indrec env sigma listdepkind mib u =
 
             (* arity in the context of the fixpoint, i.e.
                P1..P_nrec f1..f_nbconstruct *)
-	    let args = Context.Rel.to_extended_list (nrec+nbconstruct) lnamesparrec in
+	    let args = Context.Rel.to_extended_list mkRel (nrec+nbconstruct) lnamesparrec in
 	    let indf = make_ind_family((indi,u),args) in
 
 	    let arsign,_ = get_arity env indf in
@@ -337,15 +337,15 @@ let mis_make_indrec env sigma listdepkind mib u =
 
             (* constructors in context of the Cases expr, i.e.
                P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
-	    let args' = Context.Rel.to_extended_list (dect+nrec) lnamesparrec in
-	    let args'' = Context.Rel.to_extended_list ndepar lnonparrec in
+	    let args' = Context.Rel.to_extended_list mkRel (dect+nrec) lnamesparrec in
+	    let args'' = Context.Rel.to_extended_list mkRel ndepar lnonparrec in
             let indf' = make_ind_family((indi,u),args'@args'') in
 
 	    let branches =
 	      let constrs = get_constructors env indf' in
 	      let fi = Termops.rel_vect (dect-i-nctyi) nctyi in
 	      let vecfi = Array.map
-		(fun f -> appvect (f, Context.Rel.to_extended_vect ndepar lnonparrec))
+		(fun f -> appvect (f, Context.Rel.to_extended_vect mkRel ndepar lnonparrec))
 		fi
 	      in
 		Array.map3
@@ -366,9 +366,9 @@ let mis_make_indrec env sigma listdepkind mib u =
 	    let deparsign' = LocalAssum (Anonymous,depind')::arsign' in
 
 	    let pargs =
-	      let nrpar = Context.Rel.to_extended_list (2*ndepar) lnonparrec
-	      and nrar = if dep then Context.Rel.to_extended_list 0 deparsign'
-		else Context.Rel.to_extended_list 1 arsign'
+	      let nrpar = Context.Rel.to_extended_list mkRel (2*ndepar) lnonparrec
+	      and nrar = if dep then Context.Rel.to_extended_list mkRel 0 deparsign'
+		else Context.Rel.to_extended_list mkRel 1 arsign'
 	      in nrpar@nrar
 
 	    in
@@ -396,8 +396,8 @@ let mis_make_indrec env sigma listdepkind mib u =
 
 	    let typtyi =
 	      let concl =
-		let pargs = if dep then Context.Rel.to_extended_vect 0 deparsign
-		  else Context.Rel.to_extended_vect 1 arsign
+		let pargs = if dep then Context.Rel.to_extended_vect mkRel 0 deparsign
+		  else Context.Rel.to_extended_vect mkRel 1 arsign
 		in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
 	      in it_mkProd_or_LetIn_name env
 		concl
@@ -424,7 +424,7 @@ let mis_make_indrec env sigma listdepkind mib u =
 	    else
 	      let recarg = (dest_subterms recargsvec.(tyi)).(j) in
 	      let recarg = recargpar@recarg in
-	      let vargs = Context.Rel.to_extended_list (nrec+i+j) lnamesparrec in
+	      let vargs = Context.Rel.to_extended_list mkRel (nrec+i+j) lnamesparrec in
 	      let cs = get_constructor ((indi,u),mibi,mipi,vargs) (j+1) in
 	      let p_0 =
 		type_rec_branch
@@ -438,7 +438,7 @@ let mis_make_indrec env sigma listdepkind mib u =
     in
     let rec put_arity env i = function
       | ((indi,u),_,_,dep,kinds)::rest ->
-	  let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list i lnamesparrec) in
+	  let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list mkRel i lnamesparrec) in
 	  let s = 
 	    Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env) 
 	      evdref kinds 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1dcd6399e..c00ceb02e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -411,14 +411,14 @@ let build_dependent_constructor cs =
   applist
     (mkConstructU cs.cs_cstr,
      (List.map (lift cs.cs_nargs) cs.cs_params)
-      @(Context.Rel.to_extended_list 0 cs.cs_args))
+      @(Context.Rel.to_extended_list mkRel 0 cs.cs_args))
 
 let build_dependent_inductive env ((ind, params) as indf) =
   let arsign,_ = get_arity env indf in
   let nrealargs = List.length arsign in
   applist
     (mkIndU ind,
-     (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list 0 arsign))
+     (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list mkRel 0 arsign))
 
 (* builds the arity of an elimination predicate in sort [s] *)
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 9da7005e0..50ae66eb0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -289,7 +289,7 @@ let build_subclasses ~check env sigma glob pri =
       | None -> []
       | Some (rels, ((tc,u), args)) ->
 	let instapp = 
-	  Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect 0 rels)))
+	  Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels)))
 	in
 	let instapp = EConstr.Unsafe.to_constr instapp in
 	let projargs = Array.of_list (args @ [instapp]) in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1dc3ccdc0..04cc4253e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1634,7 +1634,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     | AllOccurrences, InHyp as occ ->
         let occ = if likefirst then LikeFirst else AtOccs occ in
         let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in
-        if Context.Named.Declaration.equal d newdecl
+        if Context.Named.Declaration.equal Constr.equal d newdecl
            && not (indirectly_dependent sigma c d depdecls)
         then
           if check_occs && not (in_every_hyp occs)
diff --git a/printing/printer.ml b/printing/printer.ml
index 63aeec82c..d9060c172 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -499,8 +499,8 @@ let print_evar_constraints gl sigma =
     | Some g ->
        let env = Goal.V82.env sigma g in fun e' ->
        begin
-         if Context.Named.equal (named_context env) (named_context e') then
-           if Context.Rel.equal (rel_context env) (rel_context e') then mt ()
+         if Context.Named.equal Constr.equal (named_context env) (named_context e') then
+           if Context.Rel.equal Constr.equal (rel_context env) (rel_context e') then mt ()
            else pr_rel_context_of e' sigma ++ str " |-" ++ spc ()
          else pr_context_of e' sigma ++ str " |-" ++ spc ()
        end
diff --git a/printing/printmod.ml b/printing/printmod.ml
index dfa66d437..e8ea0a99a 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -88,7 +88,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
     else Univ.Instance.empty in
   let mip = mib.mind_packets.(i) in
   let params = Inductive.inductive_paramdecls (mib,u) in
-  let args = Context.Rel.to_extended_list 0 params in
+  let args = Context.Rel.to_extended_list mkRel 0 params in
   let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
   let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
@@ -142,7 +142,7 @@ let print_record env mind mib =
   in
   let mip = mib.mind_packets.(0) in
   let params = Inductive.inductive_paramdecls (mib,u) in
-  let args = Context.Rel.to_extended_list 0 params in
+  let args = Context.Rel.to_extended_list mkRel 0 params in
   let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
   let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 142fd9a89..09b924c7e 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -228,7 +228,7 @@ let solve_by_implicit_tactic env sigma evk =
   match (!implicit_tactic, snd (evar_source evk sigma)) with
   | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
       when
-	Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
+	Context.Named.equal Constr.equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
       let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
       (try
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a4b6cb53b..ef67d28f9 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -939,7 +939,7 @@ module Search = struct
     let cwd = Lib.cwd () in
     if DirPath.equal cwd dir &&
          (onlyc == only_classes) &&
-           Context.Named.equal sign sign' &&
+           Context.Named.equal Constr.equal sign sign' &&
              Hint_db.transparent_state cached_hints == st
     then cached_hints
     else
@@ -1034,7 +1034,7 @@ module Search = struct
             (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++
                pr_ev s' (Proofview.Goal.goal gl'));
         let hints' =
-          if b && not (Context.Named.equal (Goal.hyps gl') (Goal.hyps gl))
+          if b && not (Context.Named.equal Constr.equal (Goal.hyps gl') (Goal.hyps gl))
           then
             let st = Hint_db.transparent_state info.search_hints in
             make_autogoal_hints info.search_only_classes ~st gl'
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 855273d3b..188e215a5 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -73,8 +73,8 @@ let build_dependent_inductive ind (mib,mip) =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
     (mkIndU ind,
-       Context.Rel.to_extended_list mip.mind_nrealdecls mib.mind_params_ctxt
-       @ Context.Rel.to_extended_list 0 realargs)
+       Context.Rel.to_extended_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt
+       @ Context.Rel.to_extended_list mkRel 0 realargs)
 
 let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
 let my_it_mkProd_or_LetIn s c = Term.it_mkProd_or_LetIn c s
@@ -172,7 +172,7 @@ let build_sym_scheme env ind =
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let cstr n =
-    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in
+    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect mkRel n mib.mind_params_ctxt) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
@@ -185,7 +185,7 @@ let build_sym_scheme env ind =
      my_it_mkLambda_or_LetIn_name
        (lift_rel_context (nrealargs+1) realsign_ind)
        (mkApp (mkIndU indu,Array.concat
-	  [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
+	  [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
 	   rel_vect 1 nrealargs;
 	   rel_vect (2*nrealargs+2) nrealargs])),
      mkRel 1 (* varH *),
@@ -226,13 +226,13 @@ let build_sym_involutive_scheme env ind =
     get_sym_eq_data env indu in
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
-  let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect n paramsctxt) in
+  let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect mkRel n paramsctxt) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_C =
     mkApp
       (mkIndU indu, Array.append
-         (Context.Rel.to_extended_vect (nrealargs+1) mib.mind_params_ctxt)
+         (Context.Rel.to_extended_vect mkRel (nrealargs+1) mib.mind_params_ctxt)
          (rel_vect (nrealargs+1) nrealargs)) in
   let realsign_ind =
     name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
@@ -246,15 +246,15 @@ let build_sym_involutive_scheme env ind =
 	       (mkApp (eq,[|
 	       mkApp
 	       (mkIndU indu, Array.concat
-	       [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
+	       [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
 		rel_vect (2*nrealargs+2) nrealargs;
 		rel_vect 1 nrealargs]);
                mkApp (sym,Array.concat
-	       [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
+	       [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
 		rel_vect 1 nrealargs;
 		rel_vect (2*nrealargs+2) nrealargs;
 		[|mkApp (sym,Array.concat
-		[Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
+		[Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
 		 rel_vect (2*nrealargs+2) nrealargs;
 		 rel_vect 1 nrealargs;
 		 [|mkRel 1|]])|]]);
@@ -337,7 +337,7 @@ let build_l2r_rew_scheme dep env ind kind =
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
-      Array.concat [Context.Rel.to_extended_vect n paramsctxt1;
+      Array.concat [Context.Rel.to_extended_vect mkRel n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -345,12 +345,12 @@ let build_l2r_rew_scheme dep env ind kind =
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
     mkApp (mkIndU indu, Array.concat
-       [Context.Rel.to_extended_vect (3*nrealargs) paramsctxt1;
+       [Context.Rel.to_extended_vect mkRel (3*nrealargs) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect nrealargs nrealargs]) in
   let applied_ind_G =
     mkApp (mkIndU indu, Array.concat
-       [Context.Rel.to_extended_vect (3*nrealargs+3) paramsctxt1;
+       [Context.Rel.to_extended_vect mkRel (3*nrealargs+3) paramsctxt1;
         rel_vect (nrealargs+3) nrealargs;
         rel_vect 0 nrealargs]) in
   let realsign_P = lift_rel_context nrealargs realsign in
@@ -361,10 +361,10 @@ let build_l2r_rew_scheme dep env ind kind =
                       lift_rel_context (nrealargs+3) realsign) in
   let applied_sym_C n =
      mkApp(sym,
-       Array.append (Context.Rel.to_extended_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in
+       Array.append (Context.Rel.to_extended_vect mkRel n mip.mind_arity_ctxt) [|mkVar varH|]) in
   let applied_sym_G =
      mkApp(sym,
-       Array.concat [Context.Rel.to_extended_vect (nrealargs*3+4) paramsctxt1;
+       Array.concat [Context.Rel.to_extended_vect mkRel (nrealargs*3+4) paramsctxt1;
                      rel_vect (nrealargs+4) nrealargs;
                      rel_vect 1 nrealargs;
 		     [|mkRel 1|]]) in
@@ -374,7 +374,7 @@ let build_l2r_rew_scheme dep env ind kind =
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let cieq = make_case_info (Global.env()) (fst (destInd eq)) RegularStyle in
   let applied_PC =
-    mkApp (mkVar varP,Array.append (Context.Rel.to_extended_vect 1 realsign)
+    mkApp (mkVar varP,Array.append (Context.Rel.to_extended_vect mkRel 1 realsign)
            (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in
   let applied_PG =
     mkApp (mkVar varP,Array.append (rel_vect 1 nrealargs)
@@ -384,11 +384,11 @@ let build_l2r_rew_scheme dep env ind kind =
            (if dep then [|mkRel 2|] else [||])) in
   let applied_sym_sym =
          mkApp (sym,Array.concat
-	   [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1;
+	   [Context.Rel.to_extended_vect mkRel (2*nrealargs+4) paramsctxt1;
             rel_vect 4 nrealargs;
             rel_vect (nrealargs+4) nrealargs;
             [|mkApp (sym,Array.concat
-	      [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1;
+	      [Context.Rel.to_extended_vect mkRel (2*nrealargs+4) paramsctxt1;
 	       rel_vect (nrealargs+4) nrealargs;
 	       rel_vect 4 nrealargs;
 	       [|mkRel 2|]])|]]) in
@@ -411,7 +411,7 @@ let build_l2r_rew_scheme dep env ind kind =
                    mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
                    applied_PR)),
        mkApp (sym_involutive,
-         Array.append (Context.Rel.to_extended_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
+         Array.append (Context.Rel.to_extended_vect mkRel 3 mip.mind_arity_ctxt) [|mkVar varH|]),
        [|main_body|])
    else
      main_body))))))
@@ -450,7 +450,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
     get_sym_eq_data env indu in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
-      Array.concat [Context.Rel.to_extended_vect n paramsctxt1;
+      Array.concat [Context.Rel.to_extended_vect mkRel n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -458,12 +458,12 @@ let build_l2r_forward_rew_scheme dep env ind kind =
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
     mkApp (mkIndU indu, Array.concat
-       [Context.Rel.to_extended_vect (4*nrealargs+2) paramsctxt1;
+       [Context.Rel.to_extended_vect mkRel (4*nrealargs+2) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect (nrealargs+1) nrealargs]) in
   let applied_ind_P' =
     mkApp (mkIndU indu, Array.concat
-       [Context.Rel.to_extended_vect (3*nrealargs+1) paramsctxt1;
+       [Context.Rel.to_extended_vect mkRel (3*nrealargs+1) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect (2*nrealargs+1) nrealargs]) in
   let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in
@@ -541,7 +541,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
     get_non_sym_eq_data env indu in
   let cstr n =
-    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in
+    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect mkRel n mib.mind_params_ctxt) in
   let constrargs_cstr = constrargs@[cstr 0] in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -557,8 +557,8 @@ let build_r2l_forward_rew_scheme dep env ind kind =
     applist (mkVar varP,if dep then constrargs_cstr else constrargs) in
   let applied_PG =
     mkApp (mkVar varP,
-           if dep then Context.Rel.to_extended_vect 0 realsign_ind
-	   else Context.Rel.to_extended_vect 1 realsign) in
+           if dep then Context.Rel.to_extended_vect mkRel 0 realsign_ind
+	   else Context.Rel.to_extended_vect mkRel 1 realsign) in
   let c = 
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign_ind
@@ -608,7 +608,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
 	    (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
 	      (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty
 		(EConstr.of_constr (applist (c,
-	          Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
+	          Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
       in c', ctx'
   | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme")
 
@@ -763,8 +763,8 @@ let build_congr env (eq,refl,ctx) ind =
      (mkNamedLambda varH
         (applist
            (mkIndU indu,
-	    Context.Rel.to_extended_list (mip.mind_nrealargs+2) paramsctxt @
-	    Context.Rel.to_extended_list 0 realsign))
+	    Context.Rel.to_extended_list mkRel (mip.mind_nrealargs+2) paramsctxt @
+	    Context.Rel.to_extended_list mkRel 0 realsign))
      (mkCase (ci,
        my_it_mkLambda_or_LetIn_name
 	 (lift_rel_context (mip.mind_nrealargs+3) realsign)
@@ -772,9 +772,9 @@ let build_congr env (eq,refl,ctx) ind =
            (Anonymous,
             applist
              (mkIndU indu,
-	        Context.Rel.to_extended_list (2*mip.mind_nrealdecls+3)
+	        Context.Rel.to_extended_list mkRel (2*mip.mind_nrealdecls+3)
 		  paramsctxt
-	        @ Context.Rel.to_extended_list 0 realsign),
+	        @ Context.Rel.to_extended_list mkRel 0 realsign),
             mkApp (eq,
 	      [|mkVar varB;
                 mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]);
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0ecccd5c0..8260c14ad 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1634,7 +1634,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       then
         let t = lift (i+1-n) t in
 	let abselim = beta_applist sigma (elim, params@[t;branch]) in
-	let args = Array.map EConstr.of_constr (Context.Rel.to_extended_vect 0 sign) in
+	let args = Context.Rel.to_extended_vect mkRel 0 sign in
 	let c = beta_applist sigma (abselim, [mkApp (c, args)]) in
 	  Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign)
       else
@@ -1643,8 +1643,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       (* goes from left to right when i increases! *)
       match List.nth l i with
       | Some proj ->
-	  let args = Context.Rel.to_extended_vect 0 sign in
-	  let args = Array.map EConstr.of_constr args in
+	  let args = Context.Rel.to_extended_vect mkRel 0 sign in
 	  let proj =
 	    if Environ.is_projection proj env then
 	      mkProj (Projection.make proj false, mkApp (c, args))
@@ -2190,7 +2189,7 @@ let bring_hyps hyps =
       let store = Proofview.Goal.extra gl in
       let concl = Tacmach.New.pf_nf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
-      let args = Array.map_of_list EConstr.of_constr (Context.Named.to_instance hyps) in
+      let args = Array.of_list (Context.Named.to_instance mkVar hyps) in
       Refine.refine { run = begin fun sigma ->
         let Sigma (ev, sigma, p) =
           Evarutil.new_evar env sigma ~principal:true ~store newcl in
@@ -2868,8 +2867,7 @@ let old_generalize_dep ?(with_let=false) c gl =
     (cl',project gl) in
   (** Check that the generalization is indeed well-typed *)
   let (evd, _) = Typing.type_of env evd cl'' in
-  let args = Context.Named.to_instance to_quantify_rev in
-  let args = List.map EConstr.of_constr args in
+  let args = Context.Named.to_instance mkVar to_quantify_rev in
   tclTHENLIST
     [tclEVARS evd;
      Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args));
@@ -3994,7 +3992,7 @@ let compute_scheme_signature evd scheme names_info ind_type_guess =
 	    let ind_is_ok =
 	      List.equal (fun c1 c2 -> EConstr.eq_constr evd c1 c2)
 		(List.lastn scheme.nargs indargs)
-		(List.map EConstr.of_constr (Context.Rel.to_extended_list 0 scheme.args)) in
+		(Context.Rel.to_extended_list mkRel 0 scheme.args) in
 	    if not (ccl_arg_ok && ind_is_ok) then
 	      error_ind_scheme "the conclusion of"
 	  in (cond, check_concl)
@@ -4965,7 +4963,7 @@ let abstract_subproof id gk tac =
   in
   let const, args =
     if !shrink_abstract then shrink_entry sign const
-    else (const, List.rev (Context.Named.to_instance sign))
+    else (const, List.rev (Context.Named.to_instance Constr.mkVar sign))
   in
   let args = List.map EConstr.of_constr args in
   let cd = Entries.DefinitionEntry const in
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 14071d869..f343cc73d 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -104,7 +104,7 @@ let mkFullInd (ind,u) n =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   if nparrec > 0
     then mkApp (mkIndU (ind,u),
-      Array.of_list(Context.Rel.to_extended_list (nparrec+n) lnamesparrec))
+      Array.of_list(Context.Rel.to_extended_list mkRel (nparrec+n) lnamesparrec))
     else mkIndU (ind,u)
 
 let check_bool_is_defined () =
@@ -139,7 +139,7 @@ let build_beq_scheme mode kn =
         | Name s -> Id.of_string ("eq_"^(Id.to_string s))
         | Anonymous -> Id.of_string "eq_A"
     in
-    let ext_rel_list = Context.Rel.to_extended_list 0 lnamesparrec in
+    let ext_rel_list = Context.Rel.to_extended_list mkRel 0 lnamesparrec in
       let lift_cnt = ref 0 in
       let eqs_typ = List.map (fun aa ->
                                 let a = lift !lift_cnt aa in
@@ -241,7 +241,7 @@ let build_beq_scheme mode kn =
                Cn => match Y with ... end |]  part *)
     let ci = make_case_info env (fst ind) MatchStyle in
     let constrs n = get_constructors env (make_ind_family (ind,
-      Context.Rel.to_extended_list (n+nb_ind-1) mib.mind_params_ctxt)) in
+      Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt)) in
     let constrsi = constrs (3+nparrec) in
     let n = Array.length constrsi in
     let ar = Array.make n (Lazy.force ff) in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 4c7aa01cd..95114ec39 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -194,13 +194,13 @@ let build_id_coercion idf_opt source poly =
   let val_f =
     it_mkLambda_or_LetIn
       (mkLambda (Name Namegen.default_dependent_ident,
-		 applistc vs (Context.Rel.to_extended_list 0 lams),
+		 applistc vs (Context.Rel.to_extended_list mkRel 0 lams),
 		 mkRel 1))
        lams
   in
   let typ_f =
     List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d)
-      (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list 0 lams), lift 1 t))
+      (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list mkRel 0 lams), lift 1 t))
       lams
   in
   (* juste pour verification *)
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index e24d5e74f..b898f3e83 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -39,7 +39,7 @@ let detype_param =
 let abstract_inductive hyps nparams inds =
   let ntyp = List.length inds in
   let nhyp = Context.Named.length hyps in
-  let args = Context.Named.to_instance (List.rev hyps) in
+  let args = Context.Named.to_instance mkVar (List.rev hyps) in
   let args = Array.of_list args in
   let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
   let inds' =
diff --git a/toplevel/record.ml b/toplevel/record.ml
index a65f5252e..ec719bca8 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -273,8 +273,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
   let ctx = Univ.instantiate_univ_context mib.mind_universes in
   let indu = indsp, u in
   let r = mkIndU (indsp,u) in
-  let rp = applist (r, Context.Rel.to_extended_list 0 paramdecls) in
-  let paramargs = Context.Rel.to_extended_list 1 paramdecls in (*def in [[params;x:rp]]*)
+  let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
+  let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*)
   let x = Name binder_name in
   let fields = instantiate_possibly_recursive_type indu paramdecls fields in
   let lifted_fields = Termops.lift_rel_context 1 fields in
@@ -386,7 +386,7 @@ open Typeclasses
 let declare_structure finite poly ctx id idbuild paramimpls params arity template 
     fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
-  let args = Context.Rel.to_extended_list nfields params in
+  let args = Context.Rel.to_extended_list mkRel nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
   let binder_name =