diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 14f35941..0eed1949 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -454,7 +454,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) else Evd.set_leq_sort evd s1 s2 in (evd', true) with Univ.UniverseInconsistency _ -> (evd, false) - | _ -> (evd, false)) + | e when Errors.noncritical e -> (evd, false)) | Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] -> ise_and evd @@ -730,12 +730,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let (term2,l2 as appr2) = decompose_app t2 in match kind_of_term term1, kind_of_term term2 with | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] - & array_for_all (fun a -> eq_constr a term2 or isEvar a) args1 -> + & List.for_all (fun a -> eq_constr a term2 or isEvar a) + (remove_instance_local_defs evd evk1 (Array.to_list args1)) -> (* The typical kind of constraint coming from pattern-matching return type inference *) choose_less_dependent_instance evk1 evd term2 args1 | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] - & array_for_all (fun a -> eq_constr a term1 or isEvar a) args2 -> + & List.for_all (fun a -> eq_constr a term1 or isEvar a) + (remove_instance_local_defs evd evk2 (Array.to_list args2)) -> (* The typical kind of constraint coming from pattern-matching return type inference *) choose_less_dependent_instance evk2 evd term1 args2 |