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 | |
| parent | b193c6791c16817047b34f0929b1a9817ec62ee1 (diff) | |
CLEANUP: removing unnecessary wrapper
| -rw-r--r-- | intf/vernacexpr.mli | 6 | ||||
| -rw-r--r-- | stm/stm.mli | 5 |
2 files changed, 5 insertions, 6 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 3bb86fcb2..f763ba6cf 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -286,8 +286,8 @@ type module_binder = bool option * lident list * module_ast_inl type vernac_expr = (* Control *) | VernacLoad of verbose_flag * string - | VernacTime of located_vernac_expr - | VernacRedirect of string * located_vernac_expr + | VernacTime of vernac_expr located + | VernacRedirect of string * vernac_expr located | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr | VernacError of exn (* always fails *) @@ -456,8 +456,6 @@ and tacdef_body = | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) -and located_vernac_expr = Loc.t * vernac_expr - (* A vernac classifier has to tell if a command: vernac_when: has to be executed now (alters the parser) or later vernac_type: if it is starts, ends, continues a proof or 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 |