diff options
| author | Hugo Herbelin | 2014-10-30 15:52:13 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-31 18:49:05 +0100 |
| commit | cc27d50bf7423fe1df00330eddcd81d18b55fd0f (patch) | |
| tree | d8e031956cc5250c9aca3642be8183ea675f9c03 /dev | |
| parent | 19c75f706780ea6c5bc4e22d1fbaa8ed2150ae3d (diff) | |
Enlarge the cases where the like first selection is used in destruct.
This is now a "like first" strategy iff there is no occurrences
selected in either the goal or in one of the hypotheses possibly given
in an "in" clause. Before, it was "like first" if and only if no "in"
clause was given at all.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions