diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 02:23:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 02:41:58 +0100 |
| commit | 4f52bd681ad9bbcbbd68406a58b47d8e962336ed (patch) | |
| tree | 5b891de8b42d9cb20ec3273ae1e02bd586f42fd0 /intf | |
| parent | 9f5d9cd2622f3890e70dad01898868fe29df6048 (diff) | |
Moving the Ltac definition command to an EXTEND based command.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 1a67a37d7..bd5890e29 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -379,7 +379,6 @@ type vernac_expr = | VernacBackTo of int (* Commands *) - | VernacDeclareTacticDefinition of tacdef_body list | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of obsolete_locality * string list * hints_expr |