From c78de8b5456fdaf2067b6b2d5c128923b4cda7fc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 12 Oct 2017 12:21:36 +0200
Subject: [stm] Remove all but one use of VtUnknown.

Together with #1122, this makes `VernacInstance` the only command in
the Coq codebase that cannot be statically determined to open a proof.

The reasoning for the commands moved to `VtSideff` is that
parser-altering commands should be always marked `VtNow`; the rest can
be usually marked as `VtLater`.
---
 stm/vernac_classifier.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 1ca572a36c..c5ae27a110 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -185,12 +185,12 @@ let rec classify_vernac e =
     (* These commands alter the parser *)
     | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
     | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
-    | VernacSyntaxExtension _ 
+    | VernacSyntaxExtension _
     | VernacSyntacticDefinition _
     | VernacRequire _ | VernacImport _ | VernacInclude _
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *)
-    | VernacProofMode _ 
+    | VernacProofMode _ -> VtSideff [], VtNow
     (* These are ambiguous *)
     | VernacInstance _ -> VtUnknown, VtNow
     (* Stm will install a new classifier to handle these *)
@@ -201,7 +201,7 @@ let rec classify_vernac e =
     (* What are these? *)
     | VernacToplevelControl _
     | VernacRestoreState _
-    | VernacWriteState _ -> VtUnknown, VtNow
+    | VernacWriteState _ -> VtSideff [], VtNow
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
         try List.assoc s !classifiers l ()
-- 
cgit v1.2.3