Univs: add source locations of levels

For better error messages. The API change is
backwards compatible, using a new optional argument.

3 files changed, 19 insertions, 10 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index b883db615..1276c5994 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -252,6 +252,7 @@ let instantiate_evar_array info c args =
   | _ -> replace_vars inst c
 
 type evar_universe_context = UState.t
+
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
 let empty_evar_universe_context = UState.empty
diff --git a/engine/evd.mli b/engine/evd.mli
index df491c27b..d6cf83525 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -511,6 +511,7 @@ val normalize_evar_universe_context : evar_universe_context ->
 val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level
 val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe
 val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts
+
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
 											   
 val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
@@ -568,8 +569,8 @@ val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_
 val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
 val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
 
-val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> 
-  Globnames.global_reference -> evar_map * constr
+val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
+  evar_map -> Globnames.global_reference -> evar_map * constr
 
 (********************************************************************
   Conversion w.r.t. an evar map, not unifying universes. See 
diff --git a/engine/uState.ml b/engine/uState.ml
index 8aa9a61ab..73b231851 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -49,7 +49,7 @@ let empty =
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
     uctx_universes = UGraph.initial_universes;
-    uctx_initial_universes = UGraph.initial_universes }
+    uctx_initial_universes = UGraph.initial_universes; }
 
 let make u =
     { empty with 
@@ -83,7 +83,7 @@ let union ctx ctx' =
           if local == ctx.uctx_local then ctx.uctx_universes
           else
             let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
-              UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
+            UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
 
 let context_set ctx = ctx.uctx_local
 
@@ -263,13 +263,19 @@ let universe_context ?names ctx =
        if not (Univ.LSet.is_empty left) then
          let n = Univ.LSet.cardinal left in
          let loc =
-          let get_loc u = try (Univ.LMap.find u (snd ctx.uctx_names)).uloc with Not_found -> None in
-          try List.find_map get_loc (Univ.LSet.elements left) with Not_found -> Loc.ghost
+           if n == 1 then
+             try
+               let info =
+                 Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
+               Option.default Loc.ghost info.uloc
+             with Not_found -> Loc.ghost
+           else Loc.ghost
          in
            user_err_loc (loc, "universe_context",
-                        (str(CString.plural n "Universe") ++ spc () ++
-                             Univ.LSet.pr (pr_uctx_level ctx) left ++
-                             spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound."))
+			(str(CString.plural n "Universe") ++ spc () ++
+			     Univ.LSet.pr (pr_uctx_level ctx) left ++
+			   spc () ++ str (CString.conjugate_verb_to_be n) ++
+                           str" unbound."))
       else
         let inst = Univ.Instance.of_array (Array.of_list newinst) in
         let ctx = Univ.UContext.make (inst,
@@ -329,7 +335,8 @@ let merge ?loc sideff rigid uctx ctx' =
   let initial = declare uctx.uctx_initial_universes in
   let univs = declare uctx.uctx_universes in
   let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
-    { uctx with uctx_names; uctx_local; uctx_universes; uctx_initial_universes = initial }
+  { uctx with uctx_names; uctx_local; uctx_universes;
+              uctx_initial_universes = initial }
 
 let merge_subst uctx s =
   { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }