Make the Constr.kind_of_term type parametric in sorts and universes.

4 files changed, 10 insertions, 9 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 9026800f2..094841d69 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -17,11 +17,11 @@ open Evd
 module API :
 sig
 type t
-val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term
-val kind_upto : Evd.evar_map -> constr -> (constr, types) Constr.kind_of_term
+val kind : Evd.evar_map -> t -> (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term
+val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
 val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type
 val whd_evar : Evd.evar_map -> t -> t
-val of_kind : (t, t) Constr.kind_of_term -> t
+val of_kind : (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -> t
 val of_constr : Constr.t -> t
 val to_constr : evar_map -> t -> Constr.t
 val unsafe_to_constr : t -> Constr.t
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 1ae71216f..e7287fc06 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -30,11 +30,11 @@ type rel_context = (constr, types) Context.Rel.pt
 
 (** {5 Destructors} *)
 
-val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term
+val kind : Evd.evar_map -> t -> (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term
 (** Same as {!Constr.kind} except that it expands evars and normalizes
     universes on the fly. *)
 
-val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t) Constr.kind_of_term
+val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term
 
 val to_constr : Evd.evar_map -> t -> Constr.t
 (** Returns the evar-normal form of the argument. See {!Evarutil.nf_evar}. *)
@@ -43,7 +43,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
 
 (** {5 Constructors} *)
 
-val of_kind : (t, t) Constr.kind_of_term -> t
+val of_kind : (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -> t
 (** Construct a term from a view. *)
 
 val of_constr : Constr.t -> t
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index da49d4e11..ca9591e71 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -178,7 +178,8 @@ val flush_and_check_evars :  evar_map -> constr -> Constr.constr
 (** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
     as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
     value of [e] in [sigma] is (recursively) used. *)
-val kind_of_term_upto : evar_map -> Constr.constr -> (Constr.constr,Constr.types) kind_of_term
+val kind_of_term_upto : evar_map -> Constr.constr ->
+  (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) kind_of_term
 
 (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
     [u] up to existential variable instantiation and equalisable
diff --git a/engine/universes.mli b/engine/universes.mli
index c3e2055f3..932de941a 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -76,8 +76,8 @@ val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
     {!eq_constr_univs_infer} taking kind-of-term functions, to expose
     subterms of [m] and [n], arguments. *)
 val eq_constr_univs_infer_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) ->
   UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
 
 (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]