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
---
 test-suite/success/qed_export.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/success/qed_export.v

(limited to 'test-suite/success')

diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v
new file mode 100644
index 0000000000..ee84cb94e9
--- /dev/null
+++ b/test-suite/success/qed_export.v
@@ -0,0 +1,18 @@
+Lemma a : True.
+Proof.
+assert True as H.
+  abstract (trivial) using exported_seff.
+exact H.
+Fail Qed export a_subproof.
+Qed export exported_seff.
+Check ( exported_seff : True ).
+
+Lemma b : True.
+Proof.
+assert True as H.
+  abstract (trivial) using exported_seff2.
+exact H.
+Qed.
+
+Fail Check ( exported_seff2 : True ).
+
-- 
cgit v1.2.3