diff options
| author | herbelin | 2011-10-22 21:33:18 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-22 21:33:18 +0000 |
| commit | b72a1d59a6de9e2cab121e9b2a39eb5d92d346f4 (patch) | |
| tree | e60b0f4dac3640df4bf9643699316f28f896a3d5 | |
| parent | 37aaece5f7e2e0150728a479975b7f873c5e6985 (diff) | |
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
| -rw-r--r-- | pretyping/evarconv.ml | 8 |
1 files changed, 7 insertions, 1 deletions
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 |