diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-07-06 15:22:20 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-07-06 15:22:20 +0200 |
| commit | 2face8d77628ded64f7d0a824f4b377694b9d7fd (patch) | |
| tree | 35492f58316da903c44af8fa6ee64c69b88a432b /pretyping/pretyping.mllib | |
| parent | 7df4e7d5fb011ff4dbb26884bb80ece20950b178 (diff) | |
Test case for #4203, fixed by commit a51cce36.
Diffstat (limited to 'pretyping/pretyping.mllib')
0 files changed, 0 insertions, 0 deletions