diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 01:31:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 01:57:19 +0100 |
| commit | 0af598b77a6242d796c66884477a046448ef1e21 (patch) | |
| tree | f0baff4fff51d0f6b785dafd01051aa37eb1c240 /intf | |
| parent | 8cb2040e4af40594826df97a735c38c8882934ca (diff) | |
Moving Tactic Notation to an EXTEND based command.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 36b855ec3..123b3ec1b 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -291,8 +291,6 @@ type vernac_expr = | VernacError of exn (* always fails *) (* Syntax *) - | VernacTacticNotation of - int * grammar_tactic_prod_item_expr list * raw_tactic_expr | VernacSyntaxExtension of obsolete_locality * (lstring * syntax_modifier list) | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) |