diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-27 11:42:33 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-27 11:42:33 +0100 |
| commit | 9182cdfba977eef23bd5a9db647c8227d87f59fc (patch) | |
| tree | 7c6718c17b3fd672c6256682fb7272f8399f0eab /kernel/declareops.ml | |
| parent | 34ae79e9d9ee62e306c035e274428b16564b03b3 (diff) | |
universes_of_constant: do a proper set union of body and type univs
Before the union was performed as a UContext.t union, that
concatenates the instances arrays, while one wants to avoid
duplicates.
We also assert that polymorphic constants have all constraints
in the constant_body (field const_universes), since the extra body
univs (stored in the opaque tables) are just for regular constants
processed asynchronously.
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index cf0f715be..1185c9d0a 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -66,8 +66,10 @@ let universes_of_constant otab cb = match cb.const_body with | Undef _ | Def _ -> cb.const_universes | OpaqueDef o -> - Univ.UContext.union cb.const_universes - (Univ.ContextSet.to_context (Opaqueproof.force_constraints otab o)) + let body_uctxs = Opaqueproof.force_constraints otab o in + assert(not cb.const_polymorphic || Univ.ContextSet.is_empty body_uctxs); + let uctxs = Univ.ContextSet.of_context cb.const_universes in + Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) let universes_of_polymorphic_constant otab cb = if cb.const_polymorphic then |