Merge PR#379: Introducing evar-insensitive constrs

13 files changed, 255 insertions, 204 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index ce20751abc..5a7561bf50 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -81,27 +81,27 @@ type pconstructor = constructor puniverses
 
 (* [Var] is used for named variables and [Rel] for variables as
    de Bruijn indices. *)
-type ('constr, 'types) kind_of_term =
+type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Rel       of int
   | Var       of Id.t
   | Meta      of metavariable
   | Evar      of 'constr pexistential
-  | Sort      of Sorts.t
+  | Sort      of 'sort
   | Cast      of 'constr * cast_kind * 'types
   | Prod      of Name.t * 'types * 'types
   | Lambda    of Name.t * 'types * 'constr
   | LetIn     of Name.t * 'constr * 'types * 'constr
   | App       of 'constr * 'constr array
-  | Const     of pconstant
-  | Ind       of pinductive
-  | Construct of pconstructor
+  | Const     of (constant * 'univs)
+  | Ind       of (inductive * 'univs)
+  | Construct of (constructor * 'univs)
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of projection * 'constr
 (* constr is the fixpoint of the previous type. Requires option
    -rectypes of the Caml compiler to be set *)
-type t = (t,t) kind_of_term
+type t = (t, t, Sorts.t, Instance.t) kind_of_term
 type constr = t
 
 type existential = existential_key * constr array
@@ -235,6 +235,12 @@ let mkVar id = Var id
 
 let kind c = c
 
+(* The other way around. We treat specifically smart constructors *)
+let of_kind = function
+| App (f, a) -> mkApp (f, a)
+| Cast (c, knd, t) -> mkCast (c, knd, t)
+| k -> k
+
 (****************************************************************************)
 (*              Functions to recur through subterms                         *)
 (****************************************************************************)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 7095dbe6f9..700c235e6a 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -188,7 +188,7 @@ type ('constr, 'types) pfixpoint =
 type ('constr, 'types) pcofixpoint =
     int * ('constr, 'types) prec_declaration
 
-type ('constr, 'types) kind_of_term =
+type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Rel       of int                                  (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *)
 
   | Var       of Id.t                                 (** Gallina-variable that was introduced by Vernacular-command that extends
@@ -197,7 +197,7 @@ type ('constr, 'types) kind_of_term =
 
   | Meta      of metavariable
   | Evar      of 'constr pexistential
-  | Sort      of Sorts.t
+  | Sort      of 'sort
   | Cast      of 'constr * cast_kind * 'types
   | Prod      of Name.t * 'types * 'types             (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *)
   | Lambda    of Name.t * 'types * 'constr            (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)].  *)
@@ -208,11 +208,11 @@ type ('constr, 'types) kind_of_term =
                                                           - [F] itself is not {!App}
                                                           - and [[|P1;..;Pn|]] is not empty. *)
 
-  | Const     of constant puniverses                  (** Gallina-variable that was introduced by Vernacular-command that extends the global environment
+  | Const     of (constant * 'univs)                  (** Gallina-variable that was introduced by Vernacular-command that extends the global environment
                                                           (i.e. [Parameter], or [Axiom], or [Definition], or [Theorem] etc.) *)
 
-  | Ind       of inductive puniverses                 (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
-  | Construct of constructor puniverses               (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
+  | Ind       of (inductive * 'univs)                 (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
+  | Construct of (constructor * 'univs)              (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
@@ -222,7 +222,8 @@ type ('constr, 'types) kind_of_term =
    least one argument and the function is not itself an applicative
    term *)
 
-val kind : constr -> (constr, types) kind_of_term
+val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
+val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr
 
 (** [equal a b] is true if [a] equals [b] modulo alpha, casts,
    and application grouping *)
@@ -310,13 +311,22 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
   (constr -> constr -> bool) ->
   constr -> constr -> bool
 
+val compare_head_gen_leq_with :
+  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
+  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
+  (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+  (Sorts.t -> Sorts.t -> bool) ->
+  (constr -> constr -> bool) ->
+  (constr -> constr -> bool) ->
+  constr -> constr -> bool
+
 (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2]
     like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2])
     is used,rather than {!kind}, to expose the immediate subterms of
     [c1] (resp. [c2]). *)
 val compare_head_gen_with :
-  (constr -> (constr,types) kind_of_term) ->
-  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
+  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
   (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
   (Sorts.t -> Sorts.t -> bool) ->
   (constr -> constr -> bool) ->
diff --git a/kernel/context.ml b/kernel/context.ml
index ae0388003d..abb284f226 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 955e214cb9..0c666a25d9 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 4a543f1957..9986f439af 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  *)
 
@@ -469,9 +469,11 @@ let lookup_modtype mp env =
 
 (*s Judgments. *)
 
-type unsafe_judgment = {
-  uj_val : constr;
-  uj_type : types }
+type ('constr, 'types) punsafe_judgment = {
+  uj_val : 'constr;
+  uj_type : 'types }
+
+type unsafe_judgment = (constr, types) punsafe_judgment
 
 let make_judge v tj =
   { uj_val = v;
@@ -480,10 +482,12 @@ let make_judge v tj =
 let j_val j = j.uj_val
 let j_type j = j.uj_type
 
-type unsafe_type_judgment = {
-  utj_val : constr;
+type 'types punsafe_type_judgment = {
+  utj_val : 'types;
   utj_type : sorts }
 
+type unsafe_type_judgment = types punsafe_type_judgment
+
 (*s Compilation of global declaration *)
 
 let compile_constant_body = Cbytegen.compile_constant_body false
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ea570cb4a8..b7431dbe5f 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -238,18 +238,21 @@ val keep_hyps : env -> Id.Set.t -> Context.Named.t
   actually only a datatype to store a term with its type and the type of its
   type. *)
 
-type unsafe_judgment = {
-  uj_val  : constr;
-  uj_type : types }
+type ('constr, 'types) punsafe_judgment = {
+  uj_val : 'constr;
+  uj_type : 'types }
 
-val make_judge : constr -> types -> unsafe_judgment
-val j_val  : unsafe_judgment -> constr
-val j_type : unsafe_judgment -> types
+type unsafe_judgment = (constr, types) punsafe_judgment
 
-type unsafe_type_judgment = {
-  utj_val  : constr;
+val make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment
+val j_val  : ('constr, 'types) punsafe_judgment -> 'constr
+val j_type : ('constr, 'types) punsafe_judgment -> 'types
+
+type 'types punsafe_type_judgment = {
+  utj_val : 'types;
   utj_type : sorts }
 
+type unsafe_type_judgment = types punsafe_type_judgment
 
 (** {6 Compilation of global declaration } *)
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index de97268b37..2ff4193384 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 3c4c2796ee..d8d365c347 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/kernel/term.ml b/kernel/term.ml
index 62c161be4c..e5a681375d 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -71,20 +71,21 @@ type pconstant = constant puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
-type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term =
+type ('constr, 'types, 'sort, 'univs) kind_of_term =
+  ('constr, 'types, 'sort, 'univs) Constr.kind_of_term =
   | Rel       of int
   | Var       of Id.t
   | Meta      of metavariable
   | Evar      of 'constr pexistential
-  | Sort      of sorts
+  | Sort      of 'sort
   | Cast      of 'constr * cast_kind * 'types
   | Prod      of Name.t * 'types * 'types
   | Lambda    of Name.t * 'types * 'constr
   | LetIn     of Name.t * 'constr * 'types * 'constr
   | App       of 'constr * 'constr array
-  | Const     of pconstant
-  | Ind       of pinductive
-  | Construct of pconstructor
+  | Const     of (constant * 'univs)
+  | Ind       of (inductive * 'univs)
+  | Construct of (constructor * 'univs)
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
@@ -179,8 +180,6 @@ let destMeta c = match kind_of_term c with
   | _ -> raise DestKO
 
 let isMeta c = match kind_of_term c with Meta _ -> true | _ -> false
-let isMetaOf mv c =
-  match kind_of_term c with Meta mv' -> Int.equal mv mv' | _ -> false
 
 (* Destructs a variable *)
 let destVar c = match kind_of_term c with
diff --git a/kernel/term.mli b/kernel/term.mli
index a8d9dfbfff..a9bb677050 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -68,20 +68,21 @@ type ('constr, 'types) prec_declaration =
 type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint
 type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint
 
-type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term =
+type ('constr, 'types, 'sort, 'univs) kind_of_term =
+  ('constr, 'types, 'sort, 'univs) Constr.kind_of_term =
   | Rel       of int
   | Var       of Id.t
   | Meta      of metavariable
   | Evar      of 'constr pexistential
-  | Sort      of sorts
+  | Sort      of 'sort
   | Cast      of 'constr * cast_kind * 'types
   | Prod      of Name.t * 'types * 'types
   | Lambda    of Name.t * 'types * 'constr
   | LetIn     of Name.t * 'constr * 'types * 'constr
   | App       of 'constr * 'constr array
-  | Const     of constant puniverses
-  | Ind       of inductive puniverses
-  | Construct of constructor puniverses
+  | Const     of (constant * 'univs)
+  | Ind       of (inductive * 'univs)
+  | Construct of (constructor * 'univs)
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
@@ -98,7 +99,6 @@ val isVarId : Id.t -> constr -> bool
 val isInd  : constr -> bool
 val isEvar : constr -> bool
 val isMeta : constr -> bool
-val isMetaOf : metavariable -> constr -> bool
 val isEvar_or_Meta : constr -> bool
 val isSort : constr -> bool
 val isCast : constr -> bool
@@ -444,7 +444,7 @@ val leq_constr_univs : constr UGraph.check_function
    application grouping and ignoring universe instances. *)
 val eq_constr_nounivs : constr -> constr -> bool
 
-val kind_of_term : constr -> (constr, types) kind_of_term
+val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
 (** Alias for [Constr.kind] *)
 
 val constr_ord : constr -> constr -> int
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 5071f0ad5d..5e17638152 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -13,52 +13,56 @@ open Reduction
 
 (* Type errors. *)
 
-type guard_error =
+type 'constr pguard_error =
   (* Fixpoints *)
   | NotEnoughAbstractionInFixBody
-  | RecursionNotOnInductiveType of constr
-  | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
+  | RecursionNotOnInductiveType of 'constr
+  | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (* CoFixpoints *)
-  | CodomainNotInductiveType of constr
+  | CodomainNotInductiveType of 'constr
   | NestedRecursiveOccurrences
-  | UnguardedRecursiveCall of constr
-  | RecCallInTypeOfAbstraction of constr
-  | RecCallInNonRecArgOfConstructor of constr
-  | RecCallInTypeOfDef of constr
-  | RecCallInCaseFun of constr
-  | RecCallInCaseArg of constr
-  | RecCallInCasePred of constr
-  | NotGuardedForm of constr
-  | ReturnPredicateNotCoInductive of constr
+  | UnguardedRecursiveCall of 'constr
+  | RecCallInTypeOfAbstraction of 'constr
+  | RecCallInNonRecArgOfConstructor of 'constr
+  | RecCallInTypeOfDef of 'constr
+  | RecCallInCaseFun of 'constr
+  | RecCallInCaseArg of 'constr
+  | RecCallInCasePred of 'constr
+  | NotGuardedForm of 'constr
+  | ReturnPredicateNotCoInductive of 'constr
+
+type guard_error = constr pguard_error
 
 type arity_error =
   | NonInformativeToInformative
   | StrongEliminationOnNonSmallType
   | WrongArity
 
-type type_error =
+type ('constr, 'types) ptype_error =
   | UnboundRel of int
   | UnboundVar of variable
-  | NotAType of unsafe_judgment
-  | BadAssumption of unsafe_judgment
-  | ReferenceVariables of identifier * constr
-  | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment
+  | NotAType of ('constr, 'types) punsafe_judgment
+  | BadAssumption of ('constr, 'types) punsafe_judgment
+  | ReferenceVariables of identifier * 'constr
+  | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
       * (sorts_family * sorts_family * arity_error) option
-  | CaseNotInductive of unsafe_judgment
+  | CaseNotInductive of ('constr, 'types) punsafe_judgment
   | WrongCaseInfo of pinductive * case_info
-  | NumberBranches of unsafe_judgment * int
-  | IllFormedBranch of constr * pconstructor * constr * constr
-  | Generalization of (Name.t * types) * unsafe_judgment
-  | ActualType of unsafe_judgment * types
+  | NumberBranches of ('constr, 'types) punsafe_judgment * int
+  | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
+  | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
+  | ActualType of ('constr, 'types) punsafe_judgment * 'types
   | CantApplyBadType of
-      (int * constr * constr) * unsafe_judgment * unsafe_judgment array
-  | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array
+      (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
+  | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
+  | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array
   | IllTypedRecBody of
-      int * Name.t array * unsafe_judgment array * types array
+      int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
   | UnsatisfiedConstraints of Univ.constraints
 
+type type_error = (constr, types) ptype_error
+
 exception TypeError of env * type_error
 
 let nfj env {uj_val=c;uj_type=ct} =
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 0c3a952b8d..bd6032716f 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -14,52 +14,56 @@ open Environ
 
 (*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix
     notation i*)
-type guard_error =
+type 'constr pguard_error =
   (** Fixpoints *)
   | NotEnoughAbstractionInFixBody
-  | RecursionNotOnInductiveType of constr
-  | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
+  | RecursionNotOnInductiveType of 'constr
+  | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (** CoFixpoints *)
-  | CodomainNotInductiveType of constr
+  | CodomainNotInductiveType of 'constr
   | NestedRecursiveOccurrences
-  | UnguardedRecursiveCall of constr
-  | RecCallInTypeOfAbstraction of constr
-  | RecCallInNonRecArgOfConstructor of constr
-  | RecCallInTypeOfDef of constr
-  | RecCallInCaseFun of constr
-  | RecCallInCaseArg of constr
-  | RecCallInCasePred of constr
-  | NotGuardedForm of constr
-  | ReturnPredicateNotCoInductive of constr
+  | UnguardedRecursiveCall of 'constr
+  | RecCallInTypeOfAbstraction of 'constr
+  | RecCallInNonRecArgOfConstructor of 'constr
+  | RecCallInTypeOfDef of 'constr
+  | RecCallInCaseFun of 'constr
+  | RecCallInCaseArg of 'constr
+  | RecCallInCasePred of 'constr
+  | NotGuardedForm of 'constr
+  | ReturnPredicateNotCoInductive of 'constr
+
+type guard_error = constr pguard_error
 
 type arity_error =
   | NonInformativeToInformative
   | StrongEliminationOnNonSmallType
   | WrongArity
 
-type type_error =
+type ('constr, 'types) ptype_error =
   | UnboundRel of int
   | UnboundVar of variable
-  | NotAType of unsafe_judgment
-  | BadAssumption of unsafe_judgment
-  | ReferenceVariables of identifier * constr
-  | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment
+  | NotAType of ('constr, 'types) punsafe_judgment
+  | BadAssumption of ('constr, 'types) punsafe_judgment
+  | ReferenceVariables of identifier * 'constr
+  | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
       * (sorts_family * sorts_family * arity_error) option
-  | CaseNotInductive of unsafe_judgment
+  | CaseNotInductive of ('constr, 'types) punsafe_judgment
   | WrongCaseInfo of pinductive * case_info
-  | NumberBranches of unsafe_judgment * int
-  | IllFormedBranch of constr * pconstructor * constr * constr
-  | Generalization of (Name.t * types) * unsafe_judgment
-  | ActualType of unsafe_judgment * types
+  | NumberBranches of ('constr, 'types) punsafe_judgment * int
+  | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
+  | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
+  | ActualType of ('constr, 'types) punsafe_judgment * 'types
   | CantApplyBadType of
-      (int * constr * constr) * unsafe_judgment * unsafe_judgment array
-  | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array
+      (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
+  | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
+  | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array
   | IllTypedRecBody of
-      int * Name.t array * unsafe_judgment array * types array
+      int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
   | UnsatisfiedConstraints of Univ.constraints
 
+type type_error = (constr, types) ptype_error
+
 exception TypeError of env * type_error
 
 val error_unbound_rel : env -> int -> 'a
diff --git a/kernel/vars.mli b/kernel/vars.mli
index f7535e6d8f..adeac422e0 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -75,7 +75,7 @@ val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list
 
 (** Take an index in an instance of a context and returns its index wrt to
     the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *)
-val adjust_rel_to_rel_context : Context.Rel.t -> int -> int
+val adjust_rel_to_rel_context : ('a, 'b) Context.Rel.pt -> int -> int
 
 (** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an]
     for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates