From e7b83e2a07fffaba0b19c62ef1a02c40d6ef603a Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 20 Sep 2019 18:58:51 +0200
Subject: Make `zify` does work for `Z.to_N`

---
 plugins/micromega/ZifyInst.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins')

diff --git a/plugins/micromega/ZifyInst.v b/plugins/micromega/ZifyInst.v
index 3c44113604..1217e8a5f7 100644
--- a/plugins/micromega/ZifyInst.v
+++ b/plugins/micromega/ZifyInst.v
@@ -172,6 +172,10 @@ Program Instance Op_Z_of_N : UnOp Z.of_N :=
   { TUOp := (fun x => x) ; TUOpInj := fun x => eq_refl (Z.of_N x) }.
 Add UnOp Op_Z_of_N.
 
+Instance Op_Z_to_N : UnOp Z.to_N :=
+  { TUOp := fun x => Z.max 0 x ; TUOpInj := ltac:(now intro x; destruct x) }.
+Add UnOp Op_Z_to_N.
+
 Instance Op_Z_neg : UnOp Z.neg :=
   { TUOp :=  Z.opp ; TUOpInj := (fun x => eq_refl (Zneg x))}.
 Add UnOp Op_Z_neg.
-- 
cgit v1.2.3