diff options
| author | Hugo Herbelin | 2015-03-07 13:22:11 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-03-07 13:24:57 +0100 |
| commit | 95f1e6467be41bfcdbac291a88f7c9a04474d585 (patch) | |
| tree | d3fc6f32578352712c7dddbbe5756f619bbc3359 /kernel | |
| parent | 21e439b65eab694adaccfaa39aec9415da0a4609 (diff) | |
Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar".
Not inventing a new fresh name if a non-fresh name is explicitly
given, as in v8.4.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions