diff options
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 17 |
2 files changed, 3 insertions, 18 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0fdad58309..1463901a52 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -515,12 +515,12 @@ let apply_conversion_problem_heuristic 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 = [] -> - (* The typical kind of constraint coming from patter-matching return + (* 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 = [] -> - (* The typical kind of constraint coming from patter-matching return + (* 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 diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 778fb3f0ea..870debaa77 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1057,22 +1057,7 @@ let check_evars env initial_sigma evd c = if not (Evd.mem initial_sigma evk) then let (loc,k) = evar_source evk evd in let evi = nf_evar_info sigma (Evd.find sigma evk) in - let explain = - let f (_,_,t1,t2) = - (try head_evar t1 = evk with Failure _ -> false) - or (try head_evar t2 = evk with Failure _ -> false) in - let check_several c inst = - let _,argsv = destEvar c in - let l = List.filter (eq_constr inst) (Array.to_list argsv) in - let n = List.length l in - (* Maybe should we select one instead of failing ... *) - if n >= 2 then Some (SeveralInstancesFound n) else None in - match List.filter f (snd (extract_all_conv_pbs evd)) with - | (_,_,t1,t2)::_ -> - if isEvar t2 then check_several t2 t1 - else check_several t1 t2 - | [] -> None - in error_unsolvable_implicit loc env sigma evi k explain + error_unsolvable_implicit loc env sigma evi k None | _ -> iter_constr proc_rec c in proc_rec c |