From a0e47bcf277d11ec7d2272bc5167fee898ad9016 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 2 Oct 2014 23:48:23 +0200
Subject: Implement module subtyping for polymorphic constants (errors on
 inductives). The implementation constant should have the a universe instance
 of the same length, we assume the universes are in the same order and we
 check that the definition does not add any constraints to the expected ones.
 This fixes bug #3670.

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

(limited to 'kernel/modops.ml')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 4c18ed275..859f83e05 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -35,6 +35,7 @@ type signature_mismatch_error =
   | NotConvertibleConstructorField of Id.t
   | NotConvertibleBodyField
   | NotConvertibleTypeField of env * types * types
+  | PolymorphicStatusExpected of bool
   | NotSameConstructorNamesField
   | NotSameInductiveNameInBlockField
   | FiniteInductiveFieldExpected of bool
@@ -44,6 +45,10 @@ type signature_mismatch_error =
   | RecordProjectionsExpected of Name.t list
   | NotEqualInductiveAliases
   | NoTypeConstraintExpected
+  | IncompatibleInstances
+  | IncompatibleUniverses of Univ.univ_inconsistency
+  | IncompatiblePolymorphism of env * types * types
+  | IncompatibleConstraints of Univ.constraints
 
 type module_typing_error =
   | SignatureMismatch of
-- 
cgit v1.2.3