From aeacd0cc2e30be3da42679e4d432ed00fbff6959 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Apr 2013 18:32:59 +0000
Subject: 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
---
 pretyping/evarconv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 *)
-- 
cgit v1.2.3