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/environ.ml | |
| parent | eeab61130a2867cd7f40f86a25911b27d1962d3a (diff) | |
| parent | fa4c0aab3eace78fe283f4630e4db5ed076d267e (diff) | |
Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)
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 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 |