From 7bf7c7fa9f6f79bee490b83b8912671898d03f73 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 24 Dec 2020 19:39:14 +0100
Subject: [PATCH] Add `pretty` instance for `positive`.

---
 theories/pretty.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/theories/pretty.v b/theories/pretty.v
index 004142b0..d23c7b4b 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -103,9 +103,13 @@ Instance pretty_nat : Pretty nat := λ x, pretty (N.of_nat x).
 Instance pretty_nat_inj : Inj (=@{nat}) (=) pretty.
 Proof. apply _. Qed.
 
+Instance pretty_positive : Pretty positive := λ x, pretty (Npos x).
+Instance pretty_positive_inj : Inj (=@{positive}) (=) pretty.
+Proof. apply _. Qed.
+
 Instance pretty_Z : Pretty Z := λ x,
   match x with
-  | Z0 => "0" | Zpos x => pretty (Npos x) | Zneg x => "-" +:+ pretty (Npos x)
+  | Z0 => "0" | Zpos x => pretty x | Zneg x => "-" +:+ pretty x
   end%string.
 Instance pretty_Z_inj : Inj (=@{Z}) (=) pretty.
 Proof.
-- 
GitLab