diff options
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 90490c38b..58e26de84 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -177,9 +177,11 @@ let rec classify_vernac e = | VernacComments _ -> VtSideff [], VtLater | VernacDeclareTacticDefinition l -> let open Libnames in + let open Vernacexpr in VtSideff (List.map (function - | (Ident (_,r),_,_) -> r - | (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater + | 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 *) |