diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-18 17:53:39 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-05 13:30:48 +0100 |
| commit | dc2dfc86d4e35c0fcb564709dc24c5f2c0135b2a (patch) | |
| tree | 89a03c04f2bdcf6d6234806a72d6fae20b42c3e7 /printing | |
| parent | 78551857a41a57607ecfb3fd010e0a9755f47cea (diff) | |
Sanitize universe declaration in Context (stop using a ref...)
When there is more than one variable to declare we stop trying to
attach global universes (ie monomorphic or section polymorphic) to one
of them.
Diffstat (limited to 'printing')
0 files changed, 0 insertions, 0 deletions