diff options
| author | Pierre-Marie Pédrot | 2017-05-09 10:03:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-06-13 10:32:32 +0200 |
| commit | 22ca6b0d70bb8b49aaa420f844c75592e5781c21 (patch) | |
| tree | 865c0332b3a52a1af6ae9ebc26a2e5eb07518de6 /API/API.mli | |
| parent | 6332f43dfee3efc890c5f8fdc1b5b54942c16307 (diff) | |
Turn the default behaviour of the refine primitive into the safe one.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions