From 1db8720bf624c202dcc4f1eecdcde803fed4efc2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 19 Nov 2019 14:28:37 +0100
Subject: 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.
---
 vernac/comInductive.ml | 3 ---
 vernac/record.ml       | 2 --
 2 files changed, 5 deletions(-)

(limited to 'vernac')

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 *)
-- 
cgit v1.2.3