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 /stm/vernac_classifier.ml | |
| parent | 9f5d9cd2622f3890e70dad01898868fe29df6048 (diff) | |
Moving the Ltac definition command to an EXTEND based command.
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 41b753fb8..ecaf0fb7c 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -173,13 +173,6 @@ let rec classify_vernac e = | VernacRegister _ | VernacNameSectionHypSet _ | VernacComments _ -> VtSideff [], VtLater - | VernacDeclareTacticDefinition l -> - let open Libnames in - let open Vernacexpr in - VtSideff (List.map (function - | TacticDefinition ((_,r),_) -> r - | TacticRedefinition (Ident (_,r),_) -> r - | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow (* (Local) Notations have to disappear *) |