diff options
| author | Hugo Herbelin | 2017-08-24 15:34:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:07 +0100 |
| commit | 77ef9a400cd570e0857a45c015bca0308e2a0eff (patch) | |
| tree | f17d2698af2f1e54b65da561ed7175a293a637b1 /interp/notation.mli | |
| parent | 5806b0476a1ac9b903503641cc3e2997d3e8d960 (diff) | |
User-level support for Gonthier-Ssreflect's "if t then pat then u else v".
Diffstat (limited to 'interp/notation.mli')
0 files changed, 0 insertions, 0 deletions