diff options
author | 2014-08-05 12:17:31 +0200 | |
---|---|---|
committer | 2014-08-05 16:52:13 +0200 | |
commit | d32bd531b00ee8916a003c0b62029ddffbccc35b (patch) | |
tree | 52e073aa0261fd6d966cf772608f6a51db81855f /tactics/leminv.mli | |
parent | 5cbeafc8d8a7fdf403b864c16ba9c4e7013b0d11 (diff) |
The [refine] tactic now accepts [uconstr].
Arguments of refine can hence be built by tactics instead of given in their entirety in one go.
Diffstat (limited to 'tactics/leminv.mli')
0 files changed, 0 insertions, 0 deletions