From d2c7022f0e16e6037c0d8c30c837abaad2c8194f Mon Sep 17 00:00:00 2001
From: Frederic Besson
Date: Mon, 12 Apr 2021 21:02:51 +0200
Subject: [zify] bugfix

- to zify the conclusion, we are using Tactics.apply (not rewrite)

Closes #11089

- constrain the arguments of Add Zify X to be GlobRef.t
Unset Primitive Projections so that projections are GlobRef.t.

Closes #14043

Update doc/sphinx/addendum/micromega.rst

Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
---
 test-suite/micromega/bug_11089.v | 13 +++++++++++++
 test-suite/micromega/zify.v      |  7 +++++++
 2 files changed, 20 insertions(+)
 create mode 100644 test-suite/micromega/bug_11089.v

(limited to 'test-suite')

diff --git a/test-suite/micromega/bug_11089.v b/test-suite/micromega/bug_11089.v
new file mode 100644
index 0000000000..e62b5b8d9e
--- /dev/null
+++ b/test-suite/micromega/bug_11089.v
@@ -0,0 +1,13 @@
+Require Import Lia.
+Unset Lia Cache.
+Definition t := nat.
+Goal forall (n : t), n = n.
+Proof.
+  intros.
+  lia.
+Qed.
+Goal let t' := nat in forall (n : t'), n = n.
+Proof.
+  intros.
+  lia.
+Qed.
diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v
index a12623c3c0..2ea320047d 100644
--- a/test-suite/micromega/zify.v
+++ b/test-suite/micromega/zify.v
@@ -167,6 +167,12 @@ Goal  @zero znat = 0%nat.
   reflexivity.
 Qed.
 
+Require Import ZifyBool.
+Instance Op_bool_inj : UnOp (inj : bool -> bool) :=
+  { TUOp := id; TUOpInj := fun _ => eq_refl }.
+Add Zify UnOp Op_bool_inj.
+
+
 Goal forall (x y : positive) (F : forall (P: Pos.le x y) , positive) (P : Pos.le x y),
     (F P + 1 = 1 + F P)%positive.
 Proof.
@@ -228,6 +234,7 @@ Proof.
   intros. lia.
 Qed.
 
+
 Ltac Zify.zify_pre_hook ::= unfold is_true in *.
 
 Goal forall x y : nat, is_true (Nat.eqb x 1) ->
-- 
cgit v1.2.3