From 848bc5b5fc366ab5869a2836c5ad83ab4d0f2842 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 May 2017 15:31:16 +0200
Subject: [vernac] Remove `Qed exporting` syntax.

We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.

Next step, understand why.
---
 test-suite/success/qed_export.v | 18 ------------------
 1 file changed, 18 deletions(-)
 delete mode 100644 test-suite/success/qed_export.v

(limited to 'test-suite')

diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v
deleted file mode 100644
index b3e41ab1fb..0000000000
--- a/test-suite/success/qed_export.v
+++ /dev/null
@@ -1,18 +0,0 @@
-Lemma a : True.
-Proof.
-assert True as H.
-  abstract (trivial) using exported_seff.
-exact H.
-Fail Qed exporting a_subproof.
-Qed exporting 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