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