From 9182cdfba977eef23bd5a9db647c8227d87f59fc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 27 Dec 2014 11:42:33 +0100 Subject: 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. --- kernel/declareops.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'kernel/declareops.ml') 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 -- cgit v1.2.3