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`. --- grammar/vernacextend.mlp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'grammar') diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index f6f46710c..a561ea370 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -82,7 +82,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, ploc_vala None, - <:expr< fun loc -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) + <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>) let make_fun_clauses loc s l = let map c = -- cgit v1.2.3