diff options
-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] |