diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-01 13:32:47 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:13 +0200 |
| commit | c1630c9dcdf91dc965b3c375d68e3338fb737531 (patch) | |
| tree | bf77e70bf7f401ff83563f50621712955b7aa618 /checker/environ.ml | |
| parent | 67bdc25eb69ecd485ae1c8fa2dd71d1933f355d0 (diff) | |
Univs: update checker
Diffstat (limited to 'checker/environ.ml')
| -rw-r--r-- | checker/environ.ml | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/checker/environ.ml b/checker/environ.ml index 6dbc44d6b..f8f5c29b7 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -84,13 +84,20 @@ let push_rec_types (lna,typarray,_) env = Array.fold_left (fun e assum -> push_rel assum e) env ctxt (* Universe constraints *) -let add_constraints c env = - if c == Univ.Constraint.empty then - env - else - let s = env.env_stratification in +let map_universes f env = + let s = env.env_stratification in { env with env_stratification = - { s with env_universes = Univ.merge_constraints c s.env_universes } } + { s with env_universes = f s.env_universes } } + +let add_constraints c env = + if c == Univ.Constraint.empty then env + else map_universes (Univ.merge_constraints c) env + +let push_context ?(strict=false) ctx env = + map_universes (Univ.merge_context strict ctx) env + +let push_context_set ?(strict=false) ctx env = + map_universes (Univ.merge_context_set strict ctx) env let check_constraints cst env = Univ.check_constraints cst env.env_stratification.env_universes |