From 969523467129115c5c46b0508c6d97195cc798d3 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Mon, 23 Sep 2019 19:17:17 +0200
Subject: Improvements of zify

- Fix reification of overloaded operators
  (triggers convertibility checks with existing terms)

- Zify instances need not be in hnf

- Fix specification of bool operators

- Add (limited) support for comparison

fixes #10779
---
 doc/stdlib/hidden-files | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index bc4d8b95ab..bb6df87970 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -44,6 +44,7 @@ plugins/micromega/ZCoeff.v
 plugins/micromega/ZMicromega.v
 plugins/micromega/ZifyInst.v
 plugins/micromega/ZifyBool.v
+plugins/micromega/ZifyComparison.v
 plugins/micromega/ZifyClasses.v
 plugins/micromega/Zify.v
 plugins/nsatz/Nsatz.v
-- 
cgit v1.2.3