diff options
| author | herbelin | 2013-05-14 18:37:42 +0000 |
|---|---|---|
| committer | herbelin | 2013-05-14 18:37:42 +0000 |
| commit | a8377ede7e0e1e6d2e39d16050fbe6fddc8158d4 (patch) | |
| tree | 40419ebae1c5be08874096f884ce709c61634e4b /pretyping | |
| parent | 4150e9127fab042cb5096585e2da9cb6eeb57983 (diff) | |
Fixing a regression in unification introduced in r16205 (error raised
by solve_candidates was not anymore handled at the expected time).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16524 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 1d5dda69f7..52088af389 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1082,8 +1082,9 @@ let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 = in advance, we check which of them apply *) exception NoCandidates +exception IncompatibleCandidates -let solve_candidates conv_algo env evd (evk,argsv as ev) rhs = +let solve_candidates conv_algo env evd (evk,argsv) rhs = let evi = Evd.find evd evk in let args = Array.to_list argsv in match evi.evar_candidates with @@ -1093,7 +1094,7 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs = List.map_filter (filter_compatible_candidates conv_algo env evd evi args rhs) l in match l' with - | [] -> error_cannot_unify env evd (mkEvar ev, rhs) + | [] -> raise IncompatibleCandidates | [c,evd] -> (* solve_candidates might have been called recursively in the mean *) (* time and the evar been solved by the filtering process *) @@ -1393,4 +1394,6 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) UnifFailure (evd,MetaOccurInBody evk1) | IllTypedInstance (env,t,u) -> UnifFailure (evd,InstanceNotSameType (evk1,env,t,u)) + | IncompatibleCandidates -> + UnifFailure (evd,ConversionFailed (env,mkEvar ev1,t2)) |