diff options
| author | Gaëtan Gilbert | 2018-08-28 15:21:12 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-13 15:05:57 +0200 |
| commit | ec4aa4971f7789eeccec2f38f2bb7ec976f87ede (patch) | |
| tree | dcb629e86ab9e7ee35ff5dcdd2d4e8ce085a597b /kernel/environ.ml | |
| parent | b5c9a9678b2a189edf092f4b8dbebccd49430154 (diff) | |
Do not catch already declared universes in Environ.add_universes
Include is still causing repeat declarations in add_universes_set
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index e7efa5e2c9..778c9a24dd 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 |