diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 14:18:08 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 16:52:13 +0200 |
| commit | e329ddbce4917f4cb90e038ed244698713f8f941 (patch) | |
| tree | efc70b48c97739bf7f715bb8856a55a14a851fd3 /tactics/tacsubst.ml | |
| parent | d32bd531b00ee8916a003c0b62029ddffbccc35b (diff) | |
Fix interpretation bug in [uconstr].
Substitution of the Ltac variables would only occur if the internalised [uconstr] was of the form [glob, Some expr], which is the case only in tactics defined inside a proof, but not in tactics defined in [Ltac].
Diffstat (limited to 'tactics/tacsubst.ml')
0 files changed, 0 insertions, 0 deletions