diff options
| author | Hugo Herbelin | 2015-12-05 09:51:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-05 09:51:42 +0100 |
| commit | ff8d99117f142dd6851eb7cecc0ae84ec8642fe1 (patch) | |
| tree | d739c888812b934ee7866e07a299ffcc8456ef11 /engine/termops.mli | |
| parent | e3e86829780f664ae7a81582a4c6251ceec4f622 (diff) | |
Contracting one extra beta-redex on the fly when typing branches of "match".
Diffstat (limited to 'engine/termops.mli')
0 files changed, 0 insertions, 0 deletions