diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-02-25 20:08:00 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-02-25 20:08:00 +0100 |
| commit | e4c81a456ed7279e255e0df2a73e14c77946be7e (patch) | |
| tree | ca303727da741377b06b51a946eb4b27cbd20700 /lib/future.ml | |
| parent | 2eaf2b1093c08304d34ba898d38343f20e7538e3 (diff) | |
Tacinterp: remove the is_value check in Ltac's let-in.
It fixes micromega. It is frankly a mystery to me why psatz ever work. The semantics of Ltac's match is still fishy.
Diffstat (limited to 'lib/future.ml')
0 files changed, 0 insertions, 0 deletions