From 2ded4c25e532c5dfca0483c211653768ebed01a7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 13 Jun 2019 15:39:43 +0200
Subject: UIP in SProp

---
 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 42fc6b2e45..ae5c4b6880 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -68,6 +68,7 @@ type ('constr, 'types) ptype_error =
   | UndeclaredUniverse of Level.t
   | DisallowedSProp
   | BadRelevance
+  | BadInvert
 
 type type_error = (constr, types) ptype_error
 
@@ -159,6 +160,9 @@ let error_disallowed_sprop env =
 let error_bad_relevance env =
   raise (TypeError (env, BadRelevance))
 
+let error_bad_invert env =
+  raise (TypeError (env, BadInvert))
+
 let map_pguard_error f = function
 | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody
 | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c)
@@ -202,3 +206,4 @@ let map_ptype_error f = function
 | UndeclaredUniverse l -> UndeclaredUniverse l
 | DisallowedSProp -> DisallowedSProp
 | BadRelevance -> BadRelevance
+| BadInvert -> BadInvert
-- 
cgit v1.2.3