diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 15:50:40 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 15:58:43 +0100 |
| commit | 20641795624dbb03da0401e4dc503660e5e73df6 (patch) | |
| tree | 3e4a94692a2c7ec1c722e8a8a3db94783a4cd684 /stm/vernac_classifier.ml | |
| parent | 84f54fd0923c15109910123443348c193e37fe0f (diff) | |
CLEANUP: Vernacexpr.VernacDeclareTacticDefinition
The definition of Vernacexpr.VernacDeclareTacticDefinition was changed.
The original definition allowed us to represent non-sensical value such as:
VernacDeclareTacticDefinition(Qualid ..., false, ...)
The new definition prevents that.
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 *) |