diff options
| author | Pierre-Marie Pédrot | 2019-08-08 13:48:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-25 22:14:34 +0200 |
| commit | 4838fd47542018ba61cd096c93edf45b7ef68529 (patch) | |
| tree | 918ec790b3de6b77ef8442532a69db9f2b1a76b1 /dev | |
| parent | 227fcc4dff6fbb68ad6b91387b2f36705329a57e (diff) | |
Refine the API to declare section-local universes.
The section local universes are undoubtedly ordered, but the API was requiring
an unordered ContextSet. We also move the naming one level up.
Unfortunately, some callers are currently defining the same polymorphic
universes in a section several times, notably the "Variable" command. I had
to hack around this behaviour.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions