diff options
Diffstat (limited to 'test-suite/micromega')
-rw-r--r-- | test-suite/micromega/zomicron.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 0ec1dbfbc..1f148becc 100644 --- a/test-suite/micromega/zomicron.v +++ b/test-suite/micromega/zomicron.v @@ -33,4 +33,13 @@ Lemma compact_proof : forall z, Proof. intros. lia. -Qed.
\ No newline at end of file +Qed. + +Lemma dummy_ex : exists (x:Z), x = x. +Proof. + eexists. + lia. + Unshelve. + exact Z0. +Qed. +
\ No newline at end of file |