From 59c3f672482537ae90d9b89dc482e2a84285dfdf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 Nov 2020 21:08:27 +0100
Subject: [PATCH] `Add Printing Constructor` for `max_nat` and `min_nat`.
---
theories/algebra/numbers.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/theories/algebra/numbers.v b/theories/algebra/numbers.v
index 25893ec9d..0d73b1199 100644
--- a/theories/algebra/numbers.v
+++ b/theories/algebra/numbers.v
@@ -46,6 +46,7 @@ End nat.
(** ** Natural numbers with [max] as the operation. *)
Record max_nat := MaxNat { max_nat_car : nat }.
+Add Printing Constructor max_nat.
Canonical Structure max_natO := leibnizO max_nat.
@@ -101,6 +102,7 @@ End max_nat.
(** ** Natural numbers with [min] as the operation. *)
Record min_nat := MinNat { min_nat_car : nat }.
+Add Printing Constructor min_nat.
Canonical Structure min_natO := leibnizO min_nat.
--
GitLab