diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 4 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 3 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 2 |
3 files changed, 5 insertions, 4 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 62c14f6f07..3bfcaa7f52 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -365,8 +365,7 @@ let push_constraints_to_env (_,univs) env = let add_universes strict ctx g = let g = Array.fold_left - (* Be lenient, module typing reintroduces universes and constraints due to includes *) - (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) + (fun g v -> UGraph.add_universe v strict g) g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in UGraph.merge_constraints (Univ.UContext.constraints ctx) g @@ -376,6 +375,7 @@ let push_context ?(strict=false) ctx env = let add_universes_set strict ctx g = let g = Univ.LSet.fold + (* Be lenient, module typing reintroduces universes and constraints due to includes *) (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) (Univ.ContextSet.levels ctx) g in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g 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 diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 43351737e5..f59e07098b 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -256,6 +256,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let tyj = infer_type env typ in let proofterm = Future.chain body (fun ((body,uctx),side_eff) -> + (* don't redeclare universes which are declared for the type *) + let uctx = Univ.ContextSet.diff uctx univs in let j, uctx = match trust with | Pure -> let env = push_context_set uctx env in |