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 /vernac/comInductive.ml | |
| 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 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index edb03a5c89..08a8d1b320 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -329,10 +329,7 @@ let template_polymorphism_candidate ~ctor_levels uctx params concl = if not concltemplate then false else let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in - let params, conclunivs = - IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu - in - not (Univ.LSet.is_empty conclunivs) + Option.has_some @@ IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu | Entries.Polymorphic_entry _ -> false let check_param = function |