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.
---
 plugins/funind/g_indfun.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index b317cec0d5..3e4f67498f 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -167,7 +167,7 @@ VERNAC COMMAND EXTEND Function
              (Vernacexpr.VernacFixpoint(None, List.map snd recsl))
          with
          | Vernacexpr.VtSideff ids, _ when hard ->
-             Vernacexpr.VtStartProof ("Classic", ids), Vernacexpr.VtLater
+             Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
          | x -> x ]
     -> [ do_generate_principle false (List.map snd recsl) ]
 END
-- 
cgit v1.2.3