diff options
| author | Gaëtan Gilbert | 2019-11-19 14:28:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-26 11:28:55 +0100 |
| commit | 1db8720bf624c202dcc4f1eecdcde803fed4efc2 (patch) | |
| tree | 3c762f209ff0f00aa11120488f9e6cf5a65a1118 | |
| parent | a5d124dd7c3d43a5ead81cfac30c7d1448002d56 (diff) | |
indTyping: error instead of anomaly for ill-formed template
and do not run template_candidate in the upper layers when the
template attribute is given.
This means we can use an over-approximation in the upper layer
implementation of template_candidate (returning false even in cases
which the kernel may accept) if we ever want to.
| -rw-r--r-- | kernel/indTyping.ml | 2 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 3 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
3 files changed, 1 insertions, 6 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 2b5409c1ab..c91cb39fe2 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -327,7 +327,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp in if template_check && List.for_all (fun x -> Option.is_empty x) param_levels && Univ.LSet.is_empty concl_levels then - CErrors.anomaly ~label:"polymorphic_template_ind" + CErrors.user_err Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") else TemplateArity {template_param_levels = param_levels; template_level = min_univ} 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 *) |