diff options
| author | Maxime Dénès | 2016-10-25 08:39:53 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-25 08:39:53 +0200 |
| commit | b00f7cdd1905e7d7c1f0241284f0808f8e1d2c45 (patch) | |
| tree | 24994922773f96baa2e644bbcc25ab01f686d41a /pretyping/evarconv.ml | |
| parent | b63a5cfa919fc0ebe664bbfb3add0fce387b1491 (diff) | |
| parent | 52a37da6b9e5d4e2024e31710df4e39cbd372865 (diff) | |
Merge remote-tracking branch 'github/pr/333' into v8.5
Was PR#233: Fix a bug in error printing of unif constraints
Diffstat (limited to 'pretyping/evarconv.ml')
| -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 d82d555f84..c538a137f2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1158,9 +1158,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 = @@ -1229,17 +1234,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 |