diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-07-07 04:56:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-19 01:48:30 +0200 |
| commit | de038270f72214b169d056642eb7144a79e6f126 (patch) | |
| tree | c1a5dc835f5042c79418fdbadc7b266a473b8c82 /engine/uState.ml | |
| parent | 13fb26d615cdb03a4c4841c20b108deab2de60b3 (diff) | |
Unify location handling of error functions.
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index c35f97b2e..c82c30400 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -255,8 +255,8 @@ let universe_context ?names ctx = let l = try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) with Not_found -> - user_err_loc (loc, "universe_context", - str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") + user_err ~loc "universe_context" + (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc)) pl ([], [], levels) in @@ -269,8 +269,8 @@ let universe_context ?names ctx = Option.default Loc.ghost info.uloc with Not_found -> Loc.ghost in - user_err_loc (loc, "universe_context", - (str(CString.plural n "Universe") ++ spc () ++ + user_err ~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.")) |