diff options
| author | Hugo Herbelin | 2017-03-03 14:43:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-03-03 14:44:42 +0100 |
| commit | 9133d6faece4feb675fdc9c66cebcb2bba9246a9 (patch) | |
| tree | fb5ef56768e88e111fa39c88f3ef791be4d728fa /plugins | |
| parent | 620f1918452b898d6663cabb5e0f341c7e767017 (diff) | |
CHANGES: choice over setoids and prop. ext.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions