diff options
| author | Maxime Dénès | 2017-07-13 15:05:48 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-13 15:05:48 +0200 |
| commit | e3eb17a728d7b6874e67462e8a83fac436441872 (patch) | |
| tree | c7932e27be16f4d2c20da8d61c3a61b101be7f70 /kernel/modops.ml | |
| parent | 9427b99b167842bc4a831def815c4824030d518f (diff) | |
| parent | 95d65ae4ec8c01f0b8381dfa7029bb32a552bcb0 (diff) | |
Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 24be46933e..a079bc8931 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -49,7 +49,7 @@ type signature_mismatch_error = | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types - | IncompatibleConstraints of Univ.constraints + | IncompatibleConstraints of Univ.AUContext.t type module_typing_error = | SignatureMismatch of |