From b72a1d59a6de9e2cab121e9b2a39eb5d92d346f4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 22 Oct 2011 21:33:18 +0000
Subject: Fail if some conv pbs remain after consider_remaining_unif_problems.
 This complies with consider_remaining_unif_problems being the last chance to
 solve constraints.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14582 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarconv.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f399420255..e67e17ae73 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -728,6 +728,11 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       (* Some head evar have been instantiated, or unknown kind of problem *)
       evar_conv_x ts env evd pbty t1 t2
 
+let check_problems_are_solved env evd =
+  match snd (extract_all_conv_pbs evd) with
+  | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2)
+  | _ -> ()
+
 let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
   let (evd,pbs) = extract_all_conv_pbs evd in
   let heuristic_solved_evd = List.fold_left
@@ -735,7 +740,8 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
       let evd', b = apply_conversion_problem_heuristic ts env evd pbty t1 t2 in
 	if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2))
     evd pbs in
-    Evd.fold_undefined (fun ev ev_info evd' -> match ev_info.evar_source with
+  check_problems_are_solved env heuristic_solved_evd;
+  Evd.fold_undefined (fun ev ev_info evd' -> match ev_info.evar_source with
 			  |_,ImpossibleCase -> 
 			     Evd.define ev (j_type (coq_unit_judge ())) evd'
 			  |_ -> evd') heuristic_solved_evd heuristic_solved_evd
-- 
cgit v1.2.3