diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index edb03a5c89..718e62b9b7 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 @@ -370,6 +367,14 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames (* Build the inductive entries *) let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) -> + { mind_entry_typename = indname; + mind_entry_arity = arity; + mind_entry_consnames = cnames; + mind_entry_lc = ctypes + }) + indnames arities arityconcl constructors + in + let template = List.map4 (fun indname (templatearity, _) concl (_, ctypes) -> let template_candidate () = templatearity || let ctor_levels = @@ -385,22 +390,17 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames in template_polymorphism_candidate ~ctor_levels uctx ctx_params concl in - let template = match template with + match template with | Some template -> if poly && template then user_err Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); template | None -> should_auto_template indname (template_candidate ()) - in - { mind_entry_typename = indname; - mind_entry_arity = arity; - mind_entry_template = template; - mind_entry_consnames = cnames; - mind_entry_lc = ctypes - }) + ) indnames arities arityconcl constructors in + let is_template = List.for_all (fun t -> t) template in (* Build the mutual inductive entry *) let mind_ent = { mind_entry_params = ctx_params; @@ -409,6 +409,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames mind_entry_inds = entries; mind_entry_private = if private_ind then Some false else None; mind_entry_universes = uctx; + mind_entry_template = is_template; mind_entry_cumulative = poly && cumulative; } in |