From e43c35ba795520fe111ac39a834f334753491b28 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 17 Apr 2017 10:31:29 +0200 Subject: [STM] explicit handling of parsing states DAG nodes hold now a system state and a parsing state. The latter is always passed to the parser. This paves the way to decoupling the effect of commands on the parsing state and the system state, and hence never force to interpret, say, Notation. Handling proof modes is now done explicitly in the STM, not by interpreting VernacStartLemma. Similarly Notation execution could be split in two phases in order to obtain a parsing state without fully executing it (that requires executing all commands before it). Co-authored-by: Maxime Dénès Co-authored-by: Emilio Jesus Gallego Arias --- plugins/funind/g_indfun.mlg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 8f0440a2a4..c4f8843e51 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -186,7 +186,7 @@ VERNAC COMMAND EXTEND Function (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacextend.VtSideff ids, _ when hard -> - Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) + Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) | x -> x } -> { do_generate_principle false (List.map snd recsl) } END -- cgit v1.2.3