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 /engine/namegen.mli | |
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 'engine/namegen.mli')
0 files changed, 0 insertions, 0 deletions