diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f2677acd6..cfca335d3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -246,7 +246,7 @@ let check_subtyping cumi paramsctxt env_ar inds = let env = Environ.push_context uctx env_ar in let env = Environ.push_context uctx_other env in let subtyp_constraints = - Variance.leq_constraints (CumulativityInfo.variance cumi) + CumulativityInfo.leq_constraints cumi (UContext.instance uctx) instance_other Constraint.empty in |