diff options
| author | Emilio Jesus Gallego Arias | 2017-10-12 12:21:36 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-12-09 18:57:52 +0100 |
| commit | c78de8b5456fdaf2067b6b2d5c128923b4cda7fc (patch) | |
| tree | 060fa9485775c394be3b4f86409069314194e206 /grammar | |
| parent | 319a3c230e9f9ec5a8a5bea9e07b6b8d17444ac9 (diff) | |
[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`.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/vernacextend.mlp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index f6f46710c2..a561ea3703 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 = |