diff options
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index b9cc7e5916..bc5c14c9b1 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -160,7 +160,7 @@ let classify_vernac e = | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ | VernacDeclareReduction _ - | VernacDeclareClass _ | VernacExistingInstance _ + | VernacExistingClass _ | VernacExistingInstance _ | VernacRegister _ | VernacNameSectionHypSet _ | VernacDeclareCustomEntry _ |