diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-11-27 16:48:39 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-27 16:48:39 +0100 |
commit | 4bf305af7e4688b96ec6f407b2a6f4e7e9d7a4a5 (patch) | |
tree | 5d2534ccc35ef94aa34ccd5d96064adb92955a04 /pretyping/detyping.ml | |
parent | 201b6592f7a416c5f5b42f001fc7d629951aa90e (diff) | |
parent | aa560c640eb3f1148c87c4343900138845729105 (diff) |
Merge PR #6241: [lib] Generalize Control.timeout type.
Diffstat (limited to 'pretyping/detyping.ml')
0 files changed, 0 insertions, 0 deletions