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