Merge pull request #559 from hendriktews/omit-proofsHEADmaster

Add feature to omit complete opaque proofs

1 files changed, 25 insertions, 0 deletions

diff --git a/ci/simple-tests/omit_test.v b/ci/simple-tests/omit_test.v
new file mode 100644
index 00000000..b8d177cc
--- /dev/null
+++ b/ci/simple-tests/omit_test.v
@@ -0,0 +1,25 @@
+
+Definition classical_logic : Prop := forall(P : Prop), ~~P -> P.
+
+(* automatic test marker 1 *)
+
+Lemma classic_excluded_middle :
+  (forall(P : Prop), P \/ ~ P) -> classical_logic.
+Proof.
+  intros H P H0.
+  (* automatic test marker 2 *)
+  specialize (H P).
+Abort.
+
+Lemma classic_excluded_middle :
+  (forall(P : Prop), P \/ ~ P) -> classical_logic.
+Proof using.
+  intros H P H0.
+  specialize (H P).
+  (* automatic test marker 3 *)
+  destruct H.
+    trivial.
+  contradiction.
+Qed.
+
+(* automatic test marker 4 *)