diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/vernac_classifier.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index fb6adaec5f..c4f392f201 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -202,8 +202,7 @@ let rec classify_vernac e = (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ - | VernacWriteState _ - | VernacError _ -> VtUnknown, VtNow + | VernacWriteState _ -> VtUnknown, VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () |