summaryrefslogtreecommitdiff
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarconv.ml')
-rw-r--r--pretyping/evarconv.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 20957e07..51183be3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: evarconv.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
open Pp
open Util
@@ -551,10 +551,10 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
let consider_remaining_unif_problems env evd =
let (evd,pbs) = extract_all_conv_pbs evd in
List.fold_left
- (fun (evd,b as p) (pbty,env,t1,t2) ->
- if b then apply_conversion_problem_heuristic env evd pbty t1 t2 else p)
- (evd,true)
- pbs
+ (fun evd (pbty,env,t1,t2) ->
+ let evd', b = apply_conversion_problem_heuristic env evd pbty t1 t2 in
+ if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2))
+ evd pbs
(* Main entry points *)