From 4a53151f846476f2fbe038a4ecb8e84256a26ba9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 14 Feb 2015 18:35:04 +0100
Subject: Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior

Of course such proofs cannot be processed asynchronously
---
 plugins/funind/functional_principles_proofs.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/functional_principles_proofs.ml')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index eb5221fd69..04347537f2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -989,7 +989,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   lemma_type
   (Lemmas.mk_hook (fun _ _ -> ()));
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
-  Lemmas.save_proof (Vernacexpr.Proved(false,None))
+  Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))
 
 
 
-- 
cgit v1.2.3