diff options
| author | Gaëtan Gilbert | 2018-08-28 15:20:14 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-13 15:05:57 +0200 |
| commit | b5c9a9678b2a189edf092f4b8dbebccd49430154 (patch) | |
| tree | edc940c403b3c7ed79e733bb5f62beb39216398e /kernel/indtypes.ml | |
| parent | cc66d4a0977db4994000bfc7e45937b3ccff3c93 (diff) | |
Avoid repeat univ declaration in cumulative subtyping check
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index d7eb865e0a..14decafcd3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -234,8 +234,7 @@ let check_subtyping cumi paramsctxt env_ar inds = let instance_other = Instance.of_array new_levels in let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env = Environ.push_context uctx env_ar in - let env = Environ.push_context uctx_other env in + let env = Environ.push_context uctx_other env_ar in let subtyp_constraints = CumulativityInfo.leq_constraints cumi (UContext.instance uctx) instance_other |