From 5d514890669296e5d25a342c15aa930595f3af10 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Thu, 30 Apr 2020 10:03:46 +0200
Subject: [zify] add support for Nat.le, Nat.lt and Nat.eq

Nat.le, Nat.lt and Nat.eq are aliased to le, lt and @eq nat.
The required declarations are now added in ZifyInst.
---
 test-suite/micromega/bug_12210.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/micromega/bug_12210.v

(limited to 'test-suite')

diff --git a/test-suite/micromega/bug_12210.v b/test-suite/micromega/bug_12210.v
new file mode 100644
index 0000000000..ca011def09
--- /dev/null
+++ b/test-suite/micromega/bug_12210.v
@@ -0,0 +1,19 @@
+Require Import PeanoNat Lia.
+
+Goal forall x, Nat.le x x.
+Proof.
+intros.
+lia.
+Qed.
+
+Goal forall x, Nat.lt x x -> False.
+Proof.
+intros.
+lia.
+Qed.
+
+Goal forall x, Nat.eq x x.
+Proof.
+intros.
+lia.
+Qed.
-- 
cgit v1.2.3