diff options
| author | Matthieu Sozeau | 2019-12-13 11:40:48 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-12-13 11:40:48 +0100 |
| commit | 3c24d4f6398cc80fd070c4e6dcac99670c8c1bba (patch) | |
| tree | 5196448bc356711cd3924dc7f80e2908558d9238 /kernel/indTyping.ml | |
| parent | dd47dfc29f4b38dd2b1745ecbf452c3cd459b89b (diff) | |
Use ~strict argument consistently in push_context/push_context_set intfs
One should generally push contexts with ~strict:true when the context is a monomorphic one (all univs > Set) except for template polymorphic inductives (>= Prop) and ~strict:false for universe polymorphic ones (>= Set). Includes fixes from Gaëtan's and Emilio's reviews
Diffstat (limited to 'kernel/indTyping.ml')
| -rw-r--r-- | kernel/indTyping.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index c91cb39fe2..a14d10c841 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -351,8 +351,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = let env_univs = match mie.mind_entry_universes with | 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 + 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 + push_context_set ~strict:false ctx env + else + (* In the regular case, all universes are [> Set] *) + push_context_set ~strict:true ctx env | Polymorphic_entry (_, ctx) -> push_context ctx env in |