aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorEnrico Tassi2014-12-27 11:42:33 +0100
committerEnrico Tassi2014-12-27 11:42:33 +0100
commit9182cdfba977eef23bd5a9db647c8227d87f59fc (patch)
tree7c6718c17b3fd672c6256682fb7272f8399f0eab /kernel/type_errors.mli
parent34ae79e9d9ee62e306c035e274428b16564b03b3 (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/type_errors.mli')
0 files changed, 0 insertions, 0 deletions