From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [location] Make location optional in Loc.located This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed and other times it printed nothing as the caller checked for `is_ghost` upstream. --- engine/uState.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/uState.ml') diff --git a/engine/uState.ml b/engine/uState.ml index c9653b6cd..eb1acb845 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -255,7 +255,7 @@ let universe_context ?names ctx = let l = try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) with Not_found -> - user_err ~loc ~hdr:"universe_context" + user_err ?loc ~hdr:"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) -- cgit v1.2.3