diff options
| author | herbelin | 2013-04-17 18:32:59 +0000 |
|---|---|---|
| committer | herbelin | 2013-04-17 18:32:59 +0000 |
| commit | aeacd0cc2e30be3da42679e4d432ed00fbff6959 (patch) | |
| tree | b87b63fc4cfc8462ec0dcb244dcb662b1c24766d | |
| 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
| -rw-r--r-- | pretyping/evarconv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index c4d1a72e62..19bced3442 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -871,7 +871,7 @@ let rec solve_unconstrained_evars_with_canditates evd = | Success evd -> solve_unconstrained_evars_with_canditates evd | UnifFailure _ -> aux l with - | IllTypedInstance _ as e + | IllTypedInstance _ -> aux l | e when Pretype_errors.precatchable_exception e -> aux l in (* List.rev is there to favor most dependent solutions *) (* and favor progress when used with the refine tactics *) |