diff options
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 28baa82666..76a1c190be 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -85,7 +85,7 @@ let make_labmap mp list = let check_conv_error error why cst poly f env a1 a2 = try - let cst' = f env (Environ.universes env) a1 a2 in + let cst' = f env a1 a2 in if poly then if Constraint.is_empty cst' then cst else error (IncompatiblePolymorphism (env, a1, a2)) |