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/leminv.mli | |
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/leminv.mli')
0 files changed, 0 insertions, 0 deletions