From 9f56baf7bb78a520dc2e7f5f0f94091ebf86dcaf Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Thu, 8 Sep 2016 14:19:02 +0200
Subject: 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.
---
 test-suite/micromega/zomicron.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 3f4c2407d2..239bc69360 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.
+
+
 
-- 
cgit v1.2.3