diff options
| author | Pierre-Marie Pédrot | 2016-10-26 13:07:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-26 13:07:34 +0200 |
| commit | 4a82de3b5b9d4a1a0830291b5b9a485bf2a16ded (patch) | |
| tree | 15ff7464cc5a250fbb6ed2a10887d34cfb62a8a4 /pretyping | |
| parent | 95429d01a8f47f5f9d1ecee3b452d920e1e1af22 (diff) | |
| parent | 2290dbb9c95b63e693ced647731623e64297f5c8 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3680cd777a..28600ad153 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1175,9 +1175,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = (* Some head evar have been instantiated, or unknown kind of problem *) evar_conv_x ts env evd pbty t1 t2 +let error_cannot_unify env evd pb ?reason t1 t2 = + Pretype_errors.error_cannot_unify_loc + (loc_of_conv_pb evd pb) env + evd ?reason (t1, t2) + let check_problems_are_solved env evd = match snd (extract_all_conv_pbs evd) with - | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2) + | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2 | _ -> () let max_undefined_with_candidates evd = @@ -1246,17 +1251,15 @@ let consider_remaining_unif_problems env aux evd pbs progress (pb :: stuck) end | UnifFailure (evd,reason) -> - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) - env evd ~reason (t1, t2)) + error_cannot_unify env evd pb ~reason t1 t2) | _ -> if progress then aux evd stuck false [] else match stuck with | [] -> (* We're finished *) evd | (pbty,env,t1,t2 as pb) :: _ -> - (* There remains stuck problems *) - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) - env evd (t1, t2) + (* There remains stuck problems *) + error_cannot_unify env evd pb t1 t2 in let (evd,pbs) = extract_all_conv_pbs evd in let heuristic_solved_evd = aux evd pbs false [] in |