diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-23 16:00:49 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:10 +0200 |
| commit | cc69a4697633e14fc00c9bd0858b38120645464b (patch) | |
| tree | 6a589f6916cf85bbc008ef3db788db8b90056278 /kernel/environ.ml | |
| parent | ff4d0d98ab0e0e81bd1acf9a7bf4b64913834911 (diff) | |
Univs: module constraints move to universe contexts as they might
declare new universes (e.g. with).
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index c433c0789..429aba4f7 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -197,8 +197,10 @@ let push_constraints_to_env (_,univs) env = add_constraints univs env let add_universes strict ctx g = - let g = Array.fold_left (fun g v -> Univ.add_universe v strict g) - g (Univ.Instance.to_array (Univ.UContext.instance ctx)) + let g = Array.fold_left + (* Be lenient, module typing reintroduces universes and constraints due to includes *) + (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in Univ.merge_constraints (Univ.UContext.constraints ctx) g @@ -206,8 +208,9 @@ let push_context ?(strict=false) ctx env = map_universes (add_universes strict ctx) env let add_universes_set strict ctx g = - let g = Univ.LSet.fold (fun v g -> Univ.add_universe v strict g) - (Univ.ContextSet.levels ctx) g + let g = Univ.LSet.fold + (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + (Univ.ContextSet.levels ctx) g in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g let push_context_set ?(strict=false) ctx env = |