From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 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 bb97f0171e..119ce2b359 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -111,6 +111,7 @@ type signature_mismatch_error =
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
   | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t }
+  | IncompatibleVariance
 
 type module_typing_error =
   | SignatureMismatch of
-- 
cgit v1.2.3