From 9990bea3e163850c0ac4dca982c73d2b2bc19a38 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 7 Jul 2020 14:25:20 +0200
Subject: Infrastructure for cumulative inductive syntax (no grammar extension
 yet)

---
 kernel/type_errors.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/type_errors.ml')

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index ae5c4b6880..624604976e 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -69,6 +69,7 @@ type ('constr, 'types) ptype_error =
   | DisallowedSProp
   | BadRelevance
   | BadInvert
+  | BadVariance of Level.t
 
 type type_error = (constr, types) ptype_error
 
@@ -163,6 +164,9 @@ let error_bad_relevance env =
 let error_bad_invert env =
   raise (TypeError (env, BadInvert))
 
+let error_bad_variance env u =
+  raise (TypeError (env, BadVariance u))
+
 let map_pguard_error f = function
 | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody
 | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c)
@@ -207,3 +211,4 @@ let map_ptype_error f = function
 | DisallowedSProp -> DisallowedSProp
 | BadRelevance -> BadRelevance
 | BadInvert -> BadInvert
+| BadVariance u -> BadVariance u
-- 
cgit v1.2.3