diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 17:26:18 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-17 18:46:09 +0200 |
| commit | aa5e962c9888889380ae85a7cbd82a8ac4779a0f (patch) | |
| tree | 6086365bd58c072e22efb4c5e57133338ed2d991 /grammar/tacextend.mlp | |
| parent | 5281317cb558f2b9aa6f854b9c7aeb617beba8e6 (diff) | |
Make set minimization option internal to Universes
Diffstat (limited to 'grammar/tacextend.mlp')
0 files changed, 0 insertions, 0 deletions