diff options
| author | Arnaud Spiwack | 2014-08-05 12:17:31 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-05 16:52:13 +0200 |
| commit | d32bd531b00ee8916a003c0b62029ddffbccc35b (patch) | |
| tree | 52e073aa0261fd6d966cf772608f6a51db81855f /kernel/type_errors.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 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions