diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 16:39:57 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 14:59:26 +0100 |
| commit | 51b2581d027528c8e4a347f157baf51a71b9d613 (patch) | |
| tree | 281b07df39f8f75cc4814b8447af5bde19153f6c /stm/stm.mli | |
| parent | b193c6791c16817047b34f0929b1a9817ec62ee1 (diff) | |
CLEANUP: removing unnecessary wrapper
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 0c05c93d4..2c9b983ec 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -9,6 +9,7 @@ open Vernacexpr open Names open Feedback +open Loc (** state-transaction-machine interface *) @@ -19,7 +20,7 @@ open Feedback The sentence [s] is parsed in the state [ontop]. If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) -val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(located_vernac_expr -> unit) -> +val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(vernac_expr located -> unit) -> bool -> edit_id -> string -> Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] @@ -123,7 +124,7 @@ val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ] (* Adds a new line to the document. It replaces the core of Vernac.interp. [finish] is called as the last bit of this function is the system is running interactively (-emacs or coqtop). *) -val interp : bool -> located_vernac_expr -> unit +val interp : bool -> vernac_expr located -> unit (* Queries for backward compatibility *) val current_proof_depth : unit -> int |