From 7d4b8108bc8fa6951e605cb9b42580ff6f8e583f Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Wed, 31 Aug 2016 19:12:15 +0200 Subject: Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'. If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative. --- test-suite/micromega/zomicron.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'test-suite/micromega') 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 -- cgit v1.2.3