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.
---
 engine/evd.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index df491c27b4..d6cf83525c 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 
-- 
cgit v1.2.3