diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-02 23:48:23 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-02 23:57:22 +0200 |
| commit | a0e47bcf277d11ec7d2272bc5167fee898ad9016 (patch) | |
| tree | e4323e150457f947400cd26c84ef294f33c1da97 /kernel/modops.ml | |
| parent | 0c320e79ba30bf567d4ca194bc114d733baf76e5 (diff) | |
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.
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 5 |
1 files changed, 5 insertions, 0 deletions
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 |