diff options
| author | Matej Kosik | 2015-12-16 16:39:57 +0100 |
|---|---|---|
| committer | Matej Kosik | 2016-01-11 14:59:26 +0100 |
| commit | 51b2581d027528c8e4a347f157baf51a71b9d613 (patch) | |
| tree | 281b07df39f8f75cc4814b8447af5bde19153f6c /intf | |
| parent | b193c6791c16817047b34f0929b1a9817ec62ee1 (diff) | |
CLEANUP: removing unnecessary wrapper
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 3bb86fcb20..f763ba6cf8 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 |