diff options
| -rw-r--r-- | kernel/indTyping.ml | 20 | ||||
| -rw-r--r-- | kernel/indTyping.mli | 2 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 5 |
3 files changed, 11 insertions, 16 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index cc15109f06..d48422909f 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -200,26 +200,27 @@ let unbounded_from_below u cstrs = let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl = let check_level l = Univ.LSet.mem l (Univ.ContextSet.levels uctx) && + (let () = assert (not @@ Univ.Level.is_small l) in true) && unbounded_from_below l (Univ.ContextSet.constraints uctx) && not (Univ.LSet.mem l ctor_levels) in let univs = Univ.Universe.levels concl in - let univs = - Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs - in + let univs = Univ.LSet.filter (fun l -> check_level l) univs in let fold acc = function | (LocalAssum (_, p)) -> (let c = Term.strip_prod_assum p in match kind c with | Sort (Type u) -> (match Univ.Universe.level u with - | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None + | Some l -> if Univ.LSet.mem l univs then Some l else None | None -> None) | _ -> None) :: acc | LocalDef _ -> acc in let params = List.fold_left fold [] paramsctxt in - params, univs + if Universe.is_type0m concl then Some (univs, params) + else if not @@ Univ.LSet.is_empty univs then Some (univs, params) + else None let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = if not (Universe.Set.is_empty univ_info.missing) @@ -262,14 +263,11 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i param_levels splayed_lc in - let param_levels, concl_levels = - template_polymorphic_univs ~ctor_levels ctx params min_univ - in - if List.for_all (fun x -> Option.is_empty x) param_levels - && Univ.LSet.is_empty concl_levels then + match template_polymorphic_univs ~ctor_levels ctx params min_univ with + | None -> CErrors.user_err Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") - else + | Some (_, param_levels) -> TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx } in 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 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 |