diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-29 16:50:49 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-29 20:30:43 +0200 |
| commit | d19e8bafe6cc18cc47bbb3e3f7aa0d2d719014c0 (patch) | |
| tree | 42a2c031b13056fb01e28308ca4978b3892a1a6b /pretyping/vnorm.mli | |
| parent | 0932339dbf44e4ef2b04426f7b4ac6d74b2f4f1f (diff) | |
Remove a failwith ""
Diffstat (limited to 'pretyping/vnorm.mli')
0 files changed, 0 insertions, 0 deletions