diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-17 18:32:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-17 18:32:59 +0000 |
| commit | aeacd0cc2e30be3da42679e4d432ed00fbff6959 (patch) | |
| tree | b87b63fc4cfc8462ec0dcb244dcb662b1c24766d /tactics | |
| parent | 7016b89ad2d08ec6161349e33511a0bb1d972f57 (diff) | |
Fix of r16257 in r16205 for "errors raised by check_evar_instance were
no longer trapped by solve_simple_eqn" was incomplete because
"try ... with E as e | e when f e -> ..." means
"try ... with (E as e | e) when f e -> ..." and not
"try ... with E as e | (e when f e) -> ...".
This was the cause for examples 2615.v and 2670.v failing since March 1.
The need for "as e" should have warned me. Sorry for the mistake.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16420 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions