diff options
| author | Pierre-Marie Pédrot | 2020-05-13 14:01:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-13 16:59:46 +0200 |
| commit | f71ef93aa21cd2ed4135588db3a5a3e8b42ceb39 (patch) | |
| tree | 39f979c1f1808034e6bdc15daff247a01d359c0a /kernel/environ.mli | |
| parent | d80458841316ca7edf7317ef412142e27133c931 (diff) | |
Make explicit that UGraph lower bounds are only of two kinds.
This makes the invariants in the code clearer, and also highlight this is
only required to implement template polymorphic inductive types.
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 7a46538772..79e632daa0 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -62,7 +62,7 @@ end type stratification = { env_universes : UGraph.t; env_sprop_allowed : bool; - env_universes_lbound : Univ.Level.t; + env_universes_lbound : UGraph.Bound.t; env_engagement : engagement } @@ -96,8 +96,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 universes_lbound : env -> UGraph.Bound.t +val set_universes_lbound : env -> UGraph.Bound.t -> env val rel_context : env -> Constr.rel_context val named_context : env -> Constr.named_context val named_context_val : env -> named_context_val |