aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.mli
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.mli')
-rw-r--r--stm/stm.mli2
1 files changed, 1 insertions, 1 deletions
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