diff options
| author | Arnaud Spiwack | 2014-01-31 15:05:38 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-01-31 18:30:00 +0100 |
| commit | 2ea5251fa8e203d5d5b9a1eb3f6887bafdabe155 (patch) | |
| tree | 62d0d5d129c1fade6f109e0f1e861c75b5bd455f /doc | |
| parent | 07d63bf9af363e4924ca14cb88b723c8ed2ea2dc (diff) | |
In Ltac's exact tactic: avoid checking the type of the term twice.
Following a remark by Jason Gross and Daniel Grayson.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions