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.
---
 doc/changelog/04-tactics/12213-zify-Nat.rst | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 doc/changelog/04-tactics/12213-zify-Nat.rst

(limited to 'doc')

diff --git a/doc/changelog/04-tactics/12213-zify-Nat.rst b/doc/changelog/04-tactics/12213-zify-Nat.rst
new file mode 100644
index 0000000000..8b744cd193
--- /dev/null
+++ b/doc/changelog/04-tactics/12213-zify-Nat.rst
@@ -0,0 +1,3 @@
+- **Added:**
+  The :tacn:`zify` tactic is now aware of `Nat.le`, `Nat.lt` and `Nat.eq`
+  (`#12213 <https://github.com/coq/coq/pull/12213>`_, by Frédéric Besson; fixes `#12210 <https://github.com/coq/coq/issues/12210>`_).
-- 
cgit v1.2.3