diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-21 11:11:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-21 11:11:59 +0000 |
| commit | ae819de2775d1bc30c05ac9574f13ec31a7103a8 (patch) | |
| tree | 8a10a9f1ec5a4aae1656ba23713c1949a430fc42 | |
| parent | cfba38a75b7166dfaf036833ce0b735242929ba8 (diff) | |
Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11158 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 6 |
2 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 58e9aca9e..229b40a0d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -505,12 +505,12 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 = let (term1,l1 as appr1) = decompose_app t1 in let (term2,l2 as appr2) = decompose_app t2 in match kind_of_term term1, kind_of_term term2 with - | Evar (evk1,args1), Rel _ when l1 = [] & l2 = [] -> + | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] -> (* The typical kind of constraint coming from patter-matching return type inference *) assert (array_for_all (fun a -> a = term2 or isEvar a) args1); choose_less_dependent_instance evk1 evd term2 args1, true - | Rel _, Evar (evk2,args2) when l1 = [] & l2 = [] -> + | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] -> (* The typical kind of constraint coming from patter-matching return type inference *) assert (array_for_all ((=) term1) args2); diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 108e21f67..a29dca57c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -461,8 +461,10 @@ let order_metas metas = let solve_simple_evar_eqn env evd ev rhs = let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in - if b & snd (extract_all_conv_pbs evd) = [] then evd - else error_cannot_unify env (evars_of evd) (mkEvar ev,rhs) + if not b then error_cannot_unify env (evars_of evd) (mkEvar ev,rhs); + let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in + if not b then error "Cannot solve unification constraints"; + evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] |