diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-15 22:10:08 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 13:32:33 +0200 |
| commit | 6c683786c8100259e8c78b710e4a75974ae00eba (patch) | |
| tree | 0a0dc4c63582c9ba1c64cf9c783da53fca8006af /stm/vernac_classifier.ml | |
| parent | c86c6558fcf7f8dc4a17aceed24f68f756f28ea9 (diff) | |
Remove VernacError
Diffstat (limited to 'stm/vernac_classifier.ml')
| -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 fb6adaec5..c4f392f20 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 () |