diff options
| author | Matthieu Sozeau | 2016-06-29 11:55:31 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-29 11:55:31 +0200 |
| commit | 5e979cf6020eea9fa0feaa77c7436a29443e35db (patch) | |
| tree | 7f2d28d1bfb9dfb72788b434ecada5603afecb57 /pretyping | |
| parent | 58b6784fee71a16719bc4f268dc42830c06a5c63 (diff) | |
| parent | 40ee96a0392fbc0945c48b5b134aa1be36f86225 (diff) | |
Merge branch 'bug4527' into trunk
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 912fd198b6..729006dbb4 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1225,9 +1225,9 @@ let rec solve_unconstrained_evars_with_candidates ts evd = let solve_unconstrained_impossible_cases env evd = Evd.fold_undefined (fun evk ev_info evd' -> match ev_info.evar_source with - | _,Evar_kinds.ImpossibleCase -> + | loc,Evar_kinds.ImpossibleCase -> let j, ctx = coq_unit_judge () in - let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd' ctx in + let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in let ty = j_type j in let conv_algo = evar_conv_x full_transparent_state in let evd' = check_evar_instance evd' evk ty conv_algo in |