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. --- library/libnames.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/libnames.mli') diff --git a/library/libnames.mli b/library/libnames.mli index 58d1da9d6..57013ef82 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -125,7 +125,7 @@ val eq_reference : reference -> reference -> bool val qualid_of_reference : reference -> qualid located val string_of_reference : reference -> string val pr_reference : reference -> std_ppcmds -val loc_of_reference : reference -> Loc.t +val loc_of_reference : reference -> Loc.t option val join_reference : reference -> reference -> reference (** Deprecated synonyms *) -- cgit v1.2.3