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.
---
 kernel/indTyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

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