From 28d45c2413ad24c758fca5cfb00ec4ba20935f39 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 23 Nov 2017 11:38:55 +0100 Subject: Separate vernac controls and regular commands. Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator. --- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 87609296b..2fd6f53c4 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)) + (Vernacexpr.(VernacExpr(VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 889c064b2..97066e531 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1509,7 +1509,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1524,7 +1524,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in -- cgit v1.2.3