From 8095d7d14cea6937346b960063d90cbb159612df Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Sat, 20 Jun 2020 20:45:15 +0900
Subject: Add a pre-hook mechanism for the `zify` tactic

---
 test-suite/micromega/zify.v | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v
index 8fd7398638..a12623c3c0 100644
--- a/test-suite/micromega/zify.v
+++ b/test-suite/micromega/zify.v
@@ -159,7 +159,7 @@ Require Import ZifyClasses.
 Require Import ZifyInst.
 
 Instance Zero : CstOp (@zero znat : nat) := Op_O.
-Add CstOp Zero.
+Add Zify CstOp Zero.
 
 
 Goal  @zero znat = 0%nat.
@@ -227,3 +227,12 @@ Goal forall (f : Z -> bool), negb (negb (f 0)) = f 0.
 Proof.
   intros. lia.
 Qed.
+
+Ltac Zify.zify_pre_hook ::= unfold is_true in *.
+
+Goal forall x y : nat, is_true (Nat.eqb x 1) ->
+                       is_true (Nat.eqb y 0) ->
+                       is_true (Nat.eqb (x + y) 1).
+Proof.
+lia.
+Qed.
-- 
cgit v1.2.3