From a42795cc1c2a8ed3efa9960af920ff7b16d928f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 1 Sep 2016 17:52:44 +0200
Subject: Introducing a new EConstr.t type to perform the nf_evar operation on
 demand.

---
 kernel/constr.ml  |  6 ++++++
 kernel/constr.mli | 10 ++++++++++
 2 files changed, 16 insertions(+)

(limited to 'kernel')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index ce20751abc..0ae3fb474d 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -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..c8be89fe2b 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -223,6 +223,7 @@ type ('constr, 'types) kind_of_term =
    term *)
 
 val kind : constr -> (constr, types) kind_of_term
+val of_kind : (constr, types) kind_of_term -> constr
 
 (** [equal a b] is true if [a] equals [b] modulo alpha, casts,
    and application grouping *)
@@ -310,6 +311,15 @@ 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) kind_of_term) ->
+  (constr -> (constr,types) 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
-- 
cgit v1.2.3


From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 00:29:02 +0100
Subject: Making judgment type generic over the type of inner constrs.

This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.

Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
---
 kernel/environ.ml      | 14 +++++++-----
 kernel/environ.mli     | 19 ++++++++++-------
 kernel/type_errors.ml  | 58 +++++++++++++++++++++++++++-----------------------
 kernel/type_errors.mli | 58 +++++++++++++++++++++++++++-----------------------
 4 files changed, 82 insertions(+), 67 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4a543f1957..5688813ad6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -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/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
-- 
cgit v1.2.3


From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Nov 2016 12:13:05 +0100
Subject: Reductionops now return EConstrs.

---
 kernel/term.ml  | 2 --
 kernel/term.mli | 1 -
 2 files changed, 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index 62c161be4c..3881cd12de 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -179,8 +179,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..e393adb813 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -98,7 +98,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
-- 
cgit v1.2.3


From 78a8d59b39dfcb07b94721fdcfd9241d404905d2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 15:30:02 +0100
Subject: 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.
---
 kernel/context.ml   |  69 ++++++++++++----------
 kernel/context.mli  | 160 ++++++++++++++++++++++++++++------------------------
 kernel/environ.ml   |   2 +-
 kernel/indtypes.ml  |   2 +-
 kernel/inductive.ml |   4 +-
 5 files changed, 129 insertions(+), 108 deletions(-)

(limited to 'kernel')

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 5688813ad6..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  *)
 
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
-- 
cgit v1.2.3


From ce029533a1f0fc6ac9e28d162350a64446522246 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 Mar 2017 23:05:17 +0200
Subject: Make the Constr.kind_of_term type parametric in sorts and universes.

---
 kernel/constr.ml  | 12 ++++++------
 kernel/constr.mli | 22 +++++++++++-----------
 kernel/term.ml    | 11 ++++++-----
 kernel/term.mli   | 13 +++++++------
 4 files changed, 30 insertions(+), 28 deletions(-)

(limited to 'kernel')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 0ae3fb474d..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
diff --git a/kernel/constr.mli b/kernel/constr.mli
index c8be89fe2b..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,8 +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 of_kind : (constr, types) kind_of_term -> constr
+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 *)
@@ -312,8 +312,8 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
   constr -> constr -> bool
 
 val compare_head_gen_leq_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) ->
@@ -325,8 +325,8 @@ val compare_head_gen_leq_with :
     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/term.ml b/kernel/term.ml
index 3881cd12de..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
diff --git a/kernel/term.mli b/kernel/term.mli
index e393adb813..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
@@ -443,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
-- 
cgit v1.2.3