diff options
| author | Gaëtan Gilbert | 2018-10-18 13:04:32 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-12 18:43:04 +0100 |
| commit | a44b97e3e7f4a302a5255ca9fc57ea0b81a36b7e (patch) | |
| tree | acf701c04456cb7fd91746a7ef4d05fa5544a85b /engine/uState.ml | |
| parent | 620bb4184017a8b720f6937f0cba09e93883e812 (diff) | |
Do not qualify universe names by section path.
Diffstat (limited to 'engine/uState.ml')
0 files changed, 0 insertions, 0 deletions