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/invfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0c7b0a0b08..b9d7e0d909 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1022,7 +1022,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 
 
 
-let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,None))
+let do_save () = Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))
 
 
 (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
-- 
cgit v1.2.3