diff --git a/theories/pretty.v b/theories/pretty.v
index 004142b0e0540257ff33bcda4958c64ba6e138fa..d23c7b4bdb7d90eee4fa173718c77cbc54b2d00b 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.