Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior

Of course such proofs cannot be processed asynchronously

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v
new file mode 100644
index 000000000..ee84cb94e
--- /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 ).
+