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/indTyping.ml | |
| 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/indTyping.ml')
| -rw-r--r-- | kernel/indTyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 8ac96a6481..e9687991c0 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -321,7 +321,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = if has_template_poly then (* For that particular case, we typecheck the inductive in an environment where the universes introduced by the definition are only [>= Prop] *) - let env = set_universes_lbound env Univ.Level.prop in + let env = set_universes_lbound env UGraph.Bound.Prop in push_context_set ~strict:false ctx env else (* In the regular case, all universes are [> Set] *) |