From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 kernel/modops.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/modops.mli')

diff --git a/kernel/modops.mli b/kernel/modops.mli
index e9f3db6e9..4b533c7ef 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -94,6 +94,7 @@ type signature_mismatch_error =
   | NotConvertibleConstructorField of Id.t
   | NotConvertibleBodyField
   | NotConvertibleTypeField of env * types * types
+  | CumulativeStatusExpected of bool
   | PolymorphicStatusExpected of bool
   | NotSameConstructorNamesField
   | NotSameInductiveNameInBlockField
-- 
cgit v1.2.3