From d4cdb7e41844e1bb77bac9a7b9df423364b996e2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 27 May 2016 14:02:39 +0200
Subject: Univs: add source locations of levels

For better error messages. The API change is
backwards compatible, using a new optional argument.
---
 pretyping/evarconv.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3