diff options
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 454a4b66e7..09f531ce13 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -160,11 +160,12 @@ let classify_vernac e = | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ | VernacDeclareReduction _ - | VernacDeclareClass _ | VernacDeclareInstances _ + | VernacExistingClass _ | VernacExistingInstance _ | VernacRegister _ | VernacNameSectionHypSet _ | VernacDeclareCustomEntry _ - | VernacComments _ -> VtSideff [], VtLater + | VernacComments _ + | VernacDeclareInstance _ -> VtSideff [], VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow (* (Local) Notations have to disappear *) |