diff options
Diffstat (limited to 'stm')
| -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 454a4b66e7..b9cc7e5916 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -160,7 +160,7 @@ let classify_vernac e = | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ | VernacDeclareReduction _ - | VernacDeclareClass _ | VernacDeclareInstances _ + | VernacDeclareClass _ | VernacExistingInstance _ | VernacRegister _ | VernacNameSectionHypSet _ | VernacDeclareCustomEntry _ |