From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 23:40:35 +0100
Subject: [location] Remove Loc.ghost.

Now it is a private field, locations are optional.
---
 engine/evd.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 9c40c8b715..0053324706 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -414,7 +414,7 @@ val extract_changed_conv_pbs : evar_map ->
       (Evar.Set.t -> evar_constraint -> bool) ->
       evar_map * evar_constraint list
 val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
-val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t
+val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
 
 (** The following functions return the set of evars immediately
     contained in the object; need the term to be evar-normal otherwise
-- 
cgit v1.2.3