diff options
| author | Pierre-Marie Pédrot | 2020-02-07 17:10:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-08 15:31:27 +0100 |
| commit | 6143ac9f9307b2f6863cca019a66cdcbfd52d7ce (patch) | |
| tree | 0544010e738d07d6c4e87224c27dfa07e6b894eb /kernel/indTyping.mli | |
| parent | dbd3a4c4213b3d56908a8387de93e27aaec501a4 (diff) | |
Do not hardcode specific handling of Prop levels in template poly.
We also factorize a few checks by returning an option when looking for
a potentially template universe.
Diffstat (limited to 'kernel/indTyping.mli')
| -rw-r--r-- | kernel/indTyping.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 723ba5459e..a625caec83 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -44,4 +44,4 @@ val template_polymorphic_univs : Univ.ContextSet.t -> Constr.rel_context -> Univ.Universe.t -> - Univ.Level.t option list * Univ.LSet.t + (Univ.LSet.t * Univ.Level.t option list) option |