diff options
| author | Hugo Herbelin | 2014-10-31 17:29:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-31 18:49:05 +0100 |
| commit | 1177da32723fd46a82b66ca7ffe4d13d93480da6 (patch) | |
| tree | 8d66f89beafc497e529bdcefd2372bdd23d90cba /stm/asyncTaskQueue.ml | |
| parent | 801cd9cb0559d3b78216da166044bd02348ed9af (diff) | |
Reorganization of the test for generic selection of occurrences in
clause; extended it so that an induction over "x" is considered
generic when the clause has the form "in H |-" (w/o the conclusion)
and x does not occur in the conclusion.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions