diff options
| author | Pierre-Marie Pédrot | 2016-03-20 03:00:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 03:03:55 +0100 |
| commit | 25bbce0e0cb841a7ad9d5c3e7ce33711b27bf41b (patch) | |
| tree | 52f9d461a62164034bc21fed120ca8b153cf28a0 /intf | |
| parent | 25d49062425ee080d3e8d06920d3073e7a81b603 (diff) | |
| parent | 5f703bbb8b4f439af9d76b1f6ef24162b67049c2 (diff) | |
Moving most of Ltac code to Hightactics.
This is a major step towards the pluginification of Ltac. The one important
file that is out of reach for now is Tacsubst, as it is used in an intricate way
to handle amongst other things auto hints.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 36b855ec3b..bd5890e296 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -60,7 +60,6 @@ type printable = | PrintClasses | PrintTypeClasses | PrintInstances of reference or_by_notation - | PrintLtac of reference | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions @@ -291,8 +290,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) @@ -382,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 |