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 9a8af3a58..a78323323 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -183,7 +183,7 @@ let classify_vernac e = | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ | VernacResetName _ | VernacResetInitial - | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow + | VernacBackTo _ | VernacRestart -> VtMeta, VtNow (* What are these? *) | VernacRestoreState _ | VernacWriteState _ -> VtSideff [], VtNow |