diff options
| author | Matthieu Sozeau | 2016-05-27 14:02:39 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-29 11:52:52 +0200 |
| commit | d4cdb7e41844e1bb77bac9a7b9df423364b996e2 (patch) | |
| tree | 082d76f16f315acd7f5ef4d153dcd5960f05837a /pretyping | |
| parent | 25ffe7f97a907d3508848c81c3e8dcc89559aadd (diff) | |
Univs: add source locations of levels
For better error messages. The API change is
backwards compatible, using a new optional argument.
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 |