diff options
author | Gaƫtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-09 14:00:42 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2017-09-19 10:28:03 +0200 |
commit | cd29948855c2cbd3f4065170e41f8dbe625e1921 (patch) | |
tree | e747c92a12074f2d0753b902c5fe00261d0a0fe4 /engine/evd.ml | |
parent | c2b881aae9c71a34199d2c66282512f2bdb19cf6 (diff) |
Don't lose names in UState.universe_context.
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
Diffstat (limited to 'engine/evd.ml')
-rw-r--r-- | engine/evd.ml | 25 |
1 files changed, 4 insertions, 21 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 06b257a9e..f1b5419de 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -748,27 +748,10 @@ let evar_universe_context d = d.universes let universe_context_set d = UState.context_set d.universes -let universe_context ?names evd = UState.universe_context ?names evd.universes - -open Misctypes -type universe_decl = - (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl - -let check_implication evd cstrs ctx = - let uctx = evar_universe_context evd in - let gr = UState.initial_graph uctx in - let grext = UGraph.merge_constraints cstrs gr in - let cstrs' = Univ.UContext.constraints ctx in - if UGraph.check_constraints cstrs' grext then () - else CErrors.user_err ~hdr:"check_univ_decl" - (str "Universe constraints are not implied by the ones declared.") - -let check_univ_decl evd decl = - let pl = if decl.univdecl_extensible_instance then None else Some decl.univdecl_instance in - let pl, ctx = universe_context ?names:pl evd in - if not decl.univdecl_extensible_constraints then - check_implication evd decl.univdecl_constraints ctx; - pl, ctx +let universe_context ~names ~extensible evd = + UState.universe_context ~names ~extensible evd.universes + +let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl let restrict_universe_context evd vars = { evd with universes = UState.restrict evd.universes vars } |