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. --- stm/stm.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm/stm.mli') diff --git a/stm/stm.mli b/stm/stm.mli index 30e9629c6..699b4f5ff 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -87,7 +87,7 @@ val get_current_state : unit -> Stateid.t val init : unit -> unit (* This returns the node at that position *) -val get_ast : Stateid.t -> (Vernacexpr.vernac_expr * Loc.t) option +val get_ast : Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option (* Filename *) val set_compilation_hints : string -> unit -- cgit v1.2.3