diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2016-08-31 19:12:15 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2016-08-31 19:12:15 +0200 |
| commit | 7d4b8108bc8fa6951e605cb9b42580ff6f8e583f (patch) | |
| tree | 38851b455ef429d861f46ef7fc4639233254bd1a /test-suite/micromega | |
| parent | 985e83e60b6665d17b81830aea4fce3384fe2b5a (diff) | |
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.
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 |