diff options
| author | Matthieu Sozeau | 2018-09-19 10:29:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-09-19 10:29:01 +0200 |
| commit | 6d74efabf11768ca1df3a2f3d5a65d25f7f95b01 (patch) | |
| tree | 8c5648169e305e9b4038b6f04efb5a155e2f2115 /kernel/indtypes.ml | |
| parent | eeab61130a2867cd7f40f86a25911b27d1962d3a (diff) | |
| parent | fa4c0aab3eace78fe283f4630e4db5ed076d267e (diff) | |
Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)
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 f79e5270a2..7abf8027bd 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 |