diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-11-13 09:21:04 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-11-19 10:11:45 +0100 |
| commit | 7232e8f3fc5237705b80a870a6a3ad1a4748b838 (patch) | |
| tree | c4899325e80b1c6fc34c83bef5d27ed45bad2c2f /pretyping/glob_ops.mli | |
| parent | bd2dd62ea83ff9374bd28f089b19d3abba6ac7cb (diff) | |
uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and pattern-matching.
In the syntax [let (x1,…,xn) := b in e] the name [x1…xn] were not interpreted with respect to the Ltac context. Hence typeable term would raise type-errors.
The same problem also existed in pattern-matching.
Diffstat (limited to 'pretyping/glob_ops.mli')
0 files changed, 0 insertions, 0 deletions