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. --- vernac/vernacentries.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'vernac/vernacentries.mli') diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index a559912a0..e99a62fe6 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -18,7 +18,7 @@ val vernac_require : val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - st:Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t + st:Vernacstate.t -> Vernacexpr.vernac_control Loc.located -> Vernacstate.t (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -36,3 +36,5 @@ val command_focus : unit Proof.focus_kind val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t + +val universe_polymorphism_option_name : string list -- cgit v1.2.3