diff options
| -rw-r--r-- | pretyping/evarconv.ml | 8 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 667ea458cc..c682829087 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -514,15 +514,15 @@ 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 _|Var _) when l1 = [] & l2 = [] -> + | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] + & array_for_all (fun a -> a = term2 or isEvar a) args1 -> (* The typical kind of constraint coming from pattern-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 _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] -> + | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] + & array_for_all (fun a -> a = term1 or isEvar a) args2 -> (* The typical kind of constraint coming from pattern-matching return type inference *) - assert (array_for_all ((=) term1) args2); choose_less_dependent_instance evk2 evd term1 args2, true | Evar ev1,_ when List.length l1 <= List.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index aed50c4687..fafdfe9950 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1059,7 +1059,7 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) = let evc = nf_isevar evd evi.evar_concl in let body = match evi.evar_body with Evar_defined b -> b | Evar_empty -> assert false in let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in - fst (conv_algo evenv evd Reduction.CUMUL ty evc) + add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd else evd in let (evd,pbs) = extract_changed_conv_pbs evd status_changed in |