diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-15 14:38:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-15 14:38:57 +0200 |
| commit | ba8dd1c47bcbbcd2678eca78783db7f5c95f37e7 (patch) | |
| tree | d7cba397b0f9e6ece420352b5dfba877e713d421 /pretyping/vnorm.mli | |
| parent | 44817bf722eacb0379bebc7e435bfafa503d574f (diff) | |
Test file for #4346: Set is no longer of type Type
Diffstat (limited to 'pretyping/vnorm.mli')
0 files changed, 0 insertions, 0 deletions