From db65876404c7c3a1343623cc9b4d6c2a7164dd95 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 26 Nov 2013 11:53:09 +0100 Subject: Vernac classification: allow for commands which start proofs but must be synchrone. The previous heuristic is to check whether the proof ends with Qed or not. This modification allows for commands which start proof but may produce transparent term even when the function ends with Qed. --- parsing/g_obligations.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'parsing') diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 index a0d4771f1..fe024d409 100644 --- a/parsing/g_obligations.ml4 +++ b/parsing/g_obligations.ml4 @@ -60,7 +60,7 @@ let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = open Obligations -let classify_obbl _ = Vernacexpr.VtStartProof ("Classic",[]), Vernacexpr.VtLater +let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater) VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl | [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] -> -- cgit v1.2.3