diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 3 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
2 files changed, 0 insertions, 5 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index d9201e54af..2aee9bd47f 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -396,9 +396,6 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa | Some template -> if poly && template then user_err Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); - if template && not (template_candidate ()) then - user_err Pp.(strbrk "Inductive " ++ Id.print indname ++ - str" cannot be made template polymorphic."); template | None -> should_auto_template indname (template_candidate ()) diff --git a/vernac/record.ml b/vernac/record.ml index c4254d11fb..d85b71df44 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -454,8 +454,6 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa | Some template, _ -> (* templateness explicitly requested *) if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); - if template && not (template_candidate ()) then - user_err Pp.(strbrk "record cannot be made template polymorphic on any universe"); template | None, template -> (* auto detect template *) |