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`.
---
 plugins/ltac/g_ltac.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 34fea6175b..8b9eb39837 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -471,7 +471,7 @@ END
 
 VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation
 | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
-  [ VtUnknown, VtNow ] ->
+  [ VtSideff [], VtNow ] ->
   [ fun ~atts ~st -> let open Vernacinterp in
       let n = Option.default 0 n in
       Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e;
-- 
cgit v1.2.3