diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2016-09-08 14:19:02 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2016-09-08 14:19:02 +0200 |
| commit | 9f56baf7bb78a520dc2e7f5f0f94091ebf86dcaf (patch) | |
| tree | 692212e73e902b4aacf36f23ae5b375016979158 /test-suite/micromega | |
| parent | 76a8288c37e68fd8559f903af60abf8c3f87c007 (diff) | |
Fix Bug #5073 : regression of micromega plugin
The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm)
instead of apply (__arith P1 ... Pn) which unification could fail.
Diffstat (limited to 'test-suite/micromega')
| -rw-r--r-- | test-suite/micromega/zomicron.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 3f4c2407d..239bc6936 100644 --- a/test-suite/micromega/zomicron.v +++ b/test-suite/micromega/zomicron.v @@ -82,4 +82,11 @@ Proof. lia. Qed. +(* Bug 5073 *) +Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. +Proof. + lia. +Qed. + + |