aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-12-19 10:11:26 +0100
committerPierre-Marie Pédrot2017-12-19 10:52:19 +0100
commit1de1d505dfd1c5a05a4910cfc872971087de26fb (patch)
treee276f4cbf43d9bc2a95ace51b86111852b1f53c4 /dev
parentc3e26fca1d077a2b69926df85d05e067882c40b0 (diff)
Let definitions do not create new universe constraints.
We force the upper layers to extrude the universe constraints before sending it to the kernel. This simplifies the suspicious handling of polymorphic constraints for section-local definitions.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions