diff options
| author | Maxime Dénès | 2017-04-24 14:36:45 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-24 14:36:45 +0200 |
| commit | 83d30f7aa8be369a8caf7c130d5dfa4962470eda (patch) | |
| tree | 2919bee50a58ec3810950be43cdb18d96830c0c8 /stm | |
| parent | ecff95e24e69a8761f7aa154312fdcc01f99766b (diff) | |
| parent | 6c683786c8100259e8c78b710e4a75974ae00eba (diff) | |
Merge PR#565: Remove VernacError
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 () |