From eb3f8225a286aef3a57ad876584b4a927241ff69 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 29 Jan 2019 15:44:45 +0100
Subject: Make kernel parametric on the lowest universe and fix #9294

This could be Prop (for compat with usual Coq), Set (for HoTT),
 or actually an arbitrary "i".

Take lower bound of universes into account in pretyping/engine

Reinstate proper elaboration of SProp <= l constraints:

replacing is_small with equality with lbound is _not_ semantics preserving!

lbound = Set

Elaborate template polymorphic inductives with lower bound Prop

This will make more constraints explicit

Check univ constraints with Prop as lower bound for template inductives

Restrict template polymorphic universes to those not bounded from below

Fixes #9294

fix suggested by Matthieu

Try second fix suggested by Matthieu

Take care of modifying elaboration for record declarations as well.

Rebase and export functions for debug

Remove exported functions used while debugging

Add a new typing flag "check_template" and option "-no-template-checl"

This parameterizes the new criterion on template polymorphic inductives
to allow bypassing it (necessary for backward compatibility).

Update checker to the new typing flags structure

Switch on the new template_check flag to allow old unsafe behavior in
indTyping.

This is the only change of code really impacting the kernel, together
with the commit implementing unbounded from below and parameterization
by the lower bound on universes.

Add deprecated option `Unset Template Check` allowing to make proof
scripts work with both 8.9 and 8.10 for a while

Fix `Template Check` option name and test it

Add `Unset Template Check` to Coq89.v

Cooking of inductives and template-check tests

Cleanup test-suite file for template check / universes(template) flags

cookind tests

Move test of `Unset Template Check` to the failure/ dir, but comment it
for now

Template test-suite test explanation

Overlays for PR 9918

Overlay for paramcoq

Add overlay for fiat_parsers (-no-template-check)

Add overlay for fiat_crypto_legacy

Update fiat-crypto legacy overlay

Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made.

Remove overlay that should no longer be necessary

The setting in the compat file should handle it

Remove now-merged fiat-crypto-legacy overlay

Update `Print Assumptions` to reflect the typing flag for template checking

Fix About and Print Assumptions for template poly, giving info on which
variables are actually polymorphic

Fix pretty printing to print global universe levels properly

Fix printing of template polymorphic universes

Fix pretty printing for template polymorphism on no universe

Fix interaction of template check and universes(template) flag

Fix indTyping to really check if there is any point in polymorphism: the
conclusion sort should be parameterized over at least one local universe

Indtyping fixes for template polymorphic Props

Allow explicit template polymorphism again

Adapt to new indTyping interface

Handle the case of template-polymorphic on no universes
correctly (morally Type0m univ represented as Prop).

Fix check of meaningfullness of template polymorphism in the kernel.

It is now done w.r.t the min_univ, the minimal universe inferred for the
inductive/record type, independently of the user-written annotation
which must only be larger than min_univ. This preserves compatibility
with UniMath and template-polymorphism as it has been implemented up-to
now.

Comment on identity non-template-polymorphism

Remove incorrect universes(template) attributes from ssr

simpl_fun can be meaningfully template-poly, as well as
pred_key (although the use is debatable: it could just
as well be in Prop).

Move `fun_of_simpl` coercion declaration out of section to respect
uniform inheritance

Remove incorrect uses of #[universes(template)] from the stdlib

Extraction of micromega changes due to moving an ind decl out of a section

Remove incorrect uses of #[universes(template)] from plugins

Fix test-suite files, removing incorrect #[universes(template)] attributes

Remove incorrect #[universes(template)] attributes in test-suite

Fix test-suite

Remove overlays as they have been merged upstream.
---
 kernel/declarations.ml |  5 ++++
 kernel/declareops.ml   |  1 +
 kernel/environ.ml      | 58 +++++++++++++++++++++++++++++++++--------
 kernel/environ.mli     | 10 +++++++-
 kernel/indTyping.ml    | 70 ++++++++++++++++++++++++++++++++++++++++----------
 kernel/indTyping.mli   |  9 +++++++
 kernel/mod_typing.ml   |  3 ++-
 kernel/reduction.ml    |  2 +-
 kernel/subtyping.ml    |  3 ++-
 kernel/uGraph.ml       |  8 +++---
 kernel/uGraph.mli      |  4 +--
 11 files changed, 138 insertions(+), 35 deletions(-)

(limited to 'kernel')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 8d32684b09..44676c9da5 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -87,6 +87,11 @@ type typing_flags = {
 
   indices_matter: bool;
   (** The universe of an inductive type must be above that of its indices. *)
+
+  check_template : bool;
+  (* If [false] then we don't check that the universes template-polymorphic
+     inductive parameterize on are necessarily local and unbounded from below.
+     This potentially introduces inconsistencies. *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 391b139496..7225671a1e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,6 +26,7 @@ let safe_flags oracle = {
   enable_VM = true;
   enable_native_compiler = true;
   indices_matter = true;
+  check_template = true;
 }
 
 (** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 655094e88b..4a2aeea22d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -59,8 +59,9 @@ type globals = {
 
 type stratification = {
   env_universes : UGraph.t;
-  env_engagement : engagement;
   env_sprop_allowed : bool;
+  env_universes_lbound : Univ.Level.t;
+  env_engagement : engagement
 }
 
 type val_kind =
@@ -119,9 +120,9 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = UGraph.initial_universes;
-    env_engagement = PredicativeSet;
     env_sprop_allowed = false;
-  };
+    env_universes_lbound = Univ.Level.set;
+    env_engagement = PredicativeSet };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
   indirect_pterms = Opaqueproof.empty_opaquetab;
@@ -262,8 +263,15 @@ let type_in_type env = not (typing_flags env).check_universes
 let deactivated_guard env = not (typing_flags env).check_guarded
 
 let indices_matter env = env.env_typing_flags.indices_matter
+let check_template env = env.env_typing_flags.check_template
 
 let universes env = env.env_stratification.env_universes
+let universes_lbound env = env.env_stratification.env_universes_lbound
+
+let set_universes_lbound env lbound =
+  let env_stratification = { env.env_stratification with env_universes_lbound = lbound } in
+  { env with env_stratification }
+
 let named_context env = env.env_named_context.env_named_ctx
 let named_context_val env = env.env_named_context
 let rel_context env = env.env_rel_context.env_rel_ctx
@@ -382,29 +390,30 @@ let check_constraints c env =
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
 
-let add_universes strict ctx g =
+let add_universes ~lbound ~strict ctx g =
   let g = Array.fold_left
-            (fun g v -> UGraph.add_universe v strict g)
+            (fun g v -> UGraph.add_universe ~lbound ~strict v g)
 	    g (Univ.Instance.to_array (Univ.UContext.instance ctx))
   in
     UGraph.merge_constraints (Univ.UContext.constraints ctx) g
 			   
 let push_context ?(strict=false) ctx env =
-  map_universes (add_universes strict ctx) env
+  map_universes (add_universes ~lbound:(universes_lbound env) ~strict ctx) env
 
-let add_universes_set strict ctx g =
+let add_universes_set ~lbound ~strict ctx g =
   let g = Univ.LSet.fold
             (* Be lenient, module typing reintroduces universes and constraints due to includes *)
-	    (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
+            (fun v g -> try UGraph.add_universe ~lbound ~strict v g with UGraph.AlreadyDeclared -> g)
 	    (Univ.ContextSet.levels ctx) g
   in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g
 
 let push_context_set ?(strict=false) ctx env =
-  map_universes (add_universes_set strict ctx) env
+  map_universes (add_universes_set ~lbound:(universes_lbound env) ~strict ctx) env
 
 let push_subgraph (levels,csts) env =
+  let lbound = universes_lbound env in
   let add_subgraph g =
-    let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in
+    let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) levels g in
     let newg = UGraph.merge_constraints csts newg in
     (if not (Univ.Constraint.is_empty csts) then
        let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in
@@ -428,6 +437,7 @@ let same_flags {
      share_reduction;
      enable_VM;
      enable_native_compiler;
+     check_template;
   } alt =
   check_guarded == alt.check_guarded &&
   check_positive == alt.check_positive &&
@@ -436,7 +446,8 @@ let same_flags {
   indices_matter == alt.indices_matter &&
   share_reduction == alt.share_reduction &&
   enable_VM == alt.enable_VM &&
-  enable_native_compiler == alt.enable_native_compiler
+  enable_native_compiler == alt.enable_native_compiler &&
+  check_template == alt.check_template
 [@warning "+9"]
 
 let set_typing_flags c env = (* Unsafe *)
@@ -568,11 +579,20 @@ let polymorphic_pind (ind,u) env =
 let type_in_type_ind (mind,_i) env =
   not (lookup_mind mind env).mind_typing_flags.check_universes
 
+let template_checked_ind (mind,_i) env =
+  (lookup_mind mind env).mind_typing_flags.check_template
+
 let template_polymorphic_ind (mind,i) env =
   match (lookup_mind mind env).mind_packets.(i).mind_arity with 
   | TemplateArity _ -> true
   | RegularArity _ -> false
 
+let template_polymorphic_variables (mind,i) env =
+  match (lookup_mind mind env).mind_packets.(i).mind_arity with
+  | TemplateArity { Declarations.template_param_levels = l; _ } ->
+    List.map_filter (fun level -> level) l
+  | RegularArity _ -> []
+
 let template_polymorphic_pind (ind,u) env =
   if not (Univ.Instance.is_empty u) then false
   else template_polymorphic_ind ind env
@@ -762,6 +782,22 @@ let is_template_polymorphic env r =
   | IndRef ind -> template_polymorphic_ind ind env
   | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env
 
+let get_template_polymorphic_variables env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef _id -> []
+  | ConstRef _c -> []
+  | IndRef ind -> template_polymorphic_variables ind env
+  | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env
+
+let is_template_checked env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef _id -> false
+  | ConstRef _c -> false
+  | IndRef ind -> template_checked_ind ind env
+  | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env
+
 let is_type_in_type env r =
   let open Names.GlobRef in
   match r with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index e6d814ac7d..f7de98dcfb 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -51,8 +51,9 @@ type globals
 
 type stratification = {
   env_universes : UGraph.t;
-  env_engagement : engagement;
   env_sprop_allowed : bool;
+  env_universes_lbound : Univ.Level.t;
+  env_engagement : engagement
 }
 
 type named_context_val = private {
@@ -85,6 +86,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
 val empty_env : env
 
 val universes     : env -> UGraph.t
+val universes_lbound : env -> Univ.Level.t
+val set_universes_lbound : env -> Univ.Level.t -> env
 val rel_context   : env -> Constr.rel_context
 val named_context : env -> Constr.named_context
 val named_context_val : env -> named_context_val
@@ -99,6 +102,7 @@ val is_impredicative_set : env -> bool
 val type_in_type : env -> bool
 val deactivated_guard : env -> bool
 val indices_matter : env -> bool
+val check_template : env -> bool
 
 val is_impredicative_sort : env -> Sorts.t -> bool
 val is_impredicative_univ : env -> Univ.Universe.t -> bool
@@ -254,7 +258,9 @@ val type_in_type_ind : inductive -> env -> bool
 
 (** Old-style polymorphism *)
 val template_polymorphic_ind : inductive -> env -> bool
+val template_polymorphic_variables : inductive -> env -> Univ.Level.t list
 val template_polymorphic_pind : pinductive -> env -> bool
+val template_checked_ind : inductive -> env -> bool
 
 (** {5 Modules } *)
 
@@ -346,6 +352,8 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat
 
 val is_polymorphic : env -> Names.GlobRef.t -> bool
 val is_template_polymorphic : env -> GlobRef.t -> bool
+val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list
+val is_template_checked : env -> GlobRef.t -> bool
 val is_type_in_type : env -> GlobRef.t -> bool
 
 (** Native compiler *)
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index c8e04b9fee..06d2e1bb21 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -236,22 +236,53 @@ let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_}
   if not ind_squashed then InType
   else Sorts.family (Sorts.sort_of_univ ind_univ)
 
+(* For a level to be template polymorphic, it must be introduced
+   by the definition (so have no constraint except lbound <= l)
+   and not to be constrained from below, so any universe l' <= l
+   can be used as an instance of l. All bounds from above, i.e.
+   l <=/< r will be valid for any l' <= l. *)
+let unbounded_from_below u cstrs =
+  Univ.Constraint.for_all (fun (l, d, r) ->
+      match d with
+      | Eq -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u)
+      | Lt | Le -> not (Univ.Level.equal r u))
+    cstrs
+
 (* Returns the list [x_1, ..., x_n] of levels contributing to template
-   polymorphism. The elements x_k is None if the k-th parameter (starting
-   from the most recent and ignoring let-definitions) is not contributing
-   or is Some u_k if its level is u_k and is contributing. *)
-let param_ccls paramsctxt =
+   polymorphism. The elements x_k is None if the k-th parameter
+   (starting from the most recent and ignoring let-definitions) is not
+   contributing to the inductive type's sort or is Some u_k if its level
+   is u_k and is contributing. *)
+let template_polymorphic_univs ~template_check uctx paramsctxt concl =
+  let check_level l =
+    if Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
+       unbounded_from_below l (Univ.ContextSet.constraints uctx) then
+      Some l
+    else None
+  in
+  let univs = Univ.Universe.levels concl in
+  let univs =
+    if template_check then
+      Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs
+    else univs (* Doesn't check the universes can be generalized *)
+  in
   let fold acc = function
     | (LocalAssum (_, p)) ->
       (let c = Term.strip_prod_assum p in
       match kind c with
-        | Sort (Type u) -> Univ.Universe.level u
+        | Sort (Type u) ->
+          if template_check then
+            (match Univ.Universe.level u with
+             | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None
+             | None -> None)
+          else Univ.Universe.level u
         | _ -> None) :: acc
     | LocalDef _ -> acc
   in
-  List.fold_left fold [] paramsctxt
+  let params = List.fold_left fold [] paramsctxt in
+  params, univs
 
-let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
   let arity = Vars.subst_univs_level_constr usubst arity in
   let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in
   let indices = Vars.subst_univs_level_context usubst indices in
@@ -264,14 +295,20 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
   let ind_univ = Univ.subst_univs_level_universe usubst univ_info.ind_univ in
 
   let arity = match univ_info.ind_min_univ with
-    | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ}
+    | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ}
     | Some min_univ ->
-      ((match univs with
-          | Monomorphic _ -> ()
+      let ctx = match univs with
+          | Monomorphic ctx -> ctx
           | Polymorphic _ ->
             CErrors.anomaly ~label:"polymorphic_template_ind"
-              Pp.(strbrk "Template polymorphism and full polymorphism are incompatible."));
-       TemplateArity {template_param_levels=param_ccls params; template_level=min_univ})
+              Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in
+      let param_levels, concl_levels = template_polymorphic_univs ~template_check ctx params min_univ in
+      if template_check && List.for_all (fun x -> Option.is_empty x) param_levels
+         && Univ.LSet.is_empty concl_levels then
+        CErrors.anomaly ~label:"polymorphic_template_ind"
+          Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
+      else
+        TemplateArity {template_param_levels = param_levels; template_level = min_univ}
   in
 
   let kelim = allowed_sorts univ_info in
@@ -286,10 +323,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
   mind_check_names mie;
   assert (List.is_empty (Environ.rel_context env));
 
+  let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in
+
   (* universes *)
   let env_univs =
     match mie.mind_entry_universes with
-    | Monomorphic_entry ctx -> push_context_set ctx env
+    | Monomorphic_entry ctx ->
+      let env = if has_template_poly then set_universes_lbound env Univ.Level.prop else env in
+      push_context_set ctx env
     | Polymorphic_entry (_, ctx) -> push_context ctx env
   in
 
@@ -335,7 +376,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
   (* Abstract universes *)
   let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
   let params = Vars.subst_univs_level_context usubst params in
-  let data = List.map (abstract_packets univs usubst params) data in
+  let template_check = Environ.check_template env in
+  let data = List.map (abstract_packets ~template_check univs usubst params) data in
 
   let env_ar_par =
     let ctx = Environ.rel_context env_ar_par in
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index aaa0d6a149..8da4e2885c 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -33,3 +33,12 @@ val typecheck_inductive : env -> mutual_inductive_entry ->
      (Constr.rel_context * (Constr.rel_context * Constr.types) array) *
      Sorts.family)
     array
+
+(* Utility function to compute the actual universe parameters
+   of a template polymorphic inductive *)
+val template_polymorphic_univs :
+  template_check:bool ->
+  Univ.ContextSet.t ->
+  Constr.rel_context ->
+  Univ.Universe.t ->
+  Univ.Level.t option list * Univ.LSet.t
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 9305a91731..ccc218771a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -94,7 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
           c', Monomorphic Univ.ContextSet.empty, cst
         | Polymorphic uctx, Some ctx ->
           let () =
-            if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
+            if not (UGraph.check_subtype ~lbound:(Environ.universes_lbound env)
+                      (Environ.universes env) uctx ctx) then
               error_incorrect_with_constraint lab
           in
           (** Terms are compared in a context with De Bruijn universe indices *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 53f228c618..327cb2efeb 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -777,7 +777,7 @@ let infer_cmp_universes env pb s0 s1 univs =
     | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs
     | Set, Prop -> raise NotConvertible
     | Set, Type u -> infer_pb Univ.type0_univ u
-    | Type _u, Prop -> raise NotConvertible
+    | Type u, Prop -> infer_pb u Univ.type0m_univ
     | Type u, Set -> infer_pb u Univ.type0_univ
     | Type u0, Type u1 -> infer_pb u0 u1
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d47dc0c6e1..d22ec3b7ca 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -97,7 +97,8 @@ let check_universes error env u1 u2 =
   match u1, u2 with
   | Monomorphic _, Monomorphic _ -> env
   | Polymorphic auctx1, Polymorphic auctx2 ->
-    if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+    let lbound = Environ.universes_lbound env in
+    if not (UGraph.check_subtype ~lbound (Environ.universes env) auctx2 auctx1) then
       error (IncompatibleConstraints { got = auctx1; expect = auctx2; } )
     else
       Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 6fde6e9c5f..33336079bb 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -149,10 +149,10 @@ let enforce_leq_alg u v g =
   cg
 
 exception AlreadyDeclared = G.AlreadyDeclared
-let add_universe u strict g =
+let add_universe u ~lbound ~strict g =
   let graph = G.add u g.graph in
   let d = if strict then Lt else Le in
-  enforce_constraint (Level.set,d,u) {g with graph}
+  enforce_constraint (lbound,d,u) {g with graph}
 
 let add_universe_unconstrained u g = {g with graph=G.add u g.graph}
 
@@ -164,11 +164,11 @@ let constraints_for ~kept g = G.constraints_for ~kept:(LSet.remove Level.sprop k
 
 (** Subtyping of polymorphic contexts *)
 
-let check_subtype univs ctxT ctx =
+let check_subtype ~lbound univs ctxT ctx =
   if AUContext.size ctxT == AUContext.size ctx then
     let (inst, cst) = UContext.dest (AUContext.repr ctx) in
     let cstT = UContext.constraints (AUContext.repr ctxT) in
-    let push accu v = add_universe v false accu in
+    let push accu v = add_universe v ~lbound ~strict:false accu in
     let univs = Array.fold_left push univs (Instance.to_array inst) in
     let univs = merge_constraints cstT univs in
     check_constraints cst univs
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e1b5868d55..d90f01d8d1 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -48,7 +48,7 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
 
 exception AlreadyDeclared
 
-val add_universe : Level.t -> bool -> t -> t
+val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t
 
 (** Add a universe without (Prop,Set) <= u *)
 val add_universe_unconstrained : Level.t -> t -> t
@@ -86,7 +86,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t
 val domain : t -> LSet.t
 (** Known universes *)
 
-val check_subtype : AUContext.t check_function
+val check_subtype : lbound:Level.t -> AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)
 
-- 
cgit v1.2.3