From 14224b1799fe78c14f6d35b56ef14bcbdc9694b7 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi <pi8027@gmail.com>
Date: Tue, 23 May 2023 14:46:26 +0200
Subject: [PATCH] Replace Order.bottom and Order.top with \bot and \top

---
 theories/zify_ssreflect.v | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/theories/zify_ssreflect.v b/theories/zify_ssreflect.v
index de0bbdd..2b66a17 100644
--- a/theories/zify_ssreflect.v
+++ b/theories/zify_ssreflect.v
@@ -117,19 +117,19 @@ Instance Op_bool_join' : BinOp (Order.meet : bool^d -> _) := Op_orb.
 Add Zify BinOp Op_bool_join'.
 
 #[global]
-Instance Op_bool_bottom : CstOp (Order.bottom : bool) := Op_false.
+Instance Op_bool_bottom : CstOp (\bot : bool)%O := Op_false.
 Add Zify CstOp Op_bool_bottom.
 
 #[global]
-Instance Op_bool_bottom' : CstOp (Order.top : bool^d) := Op_false.
+Instance Op_bool_bottom' : CstOp (\top : bool^d)%O := Op_false.
 Add Zify CstOp Op_bool_bottom'.
 
 #[global]
-Instance Op_bool_top : CstOp (Order.top : bool) := Op_true.
+Instance Op_bool_top : CstOp (\top : bool)%O := Op_true.
 Add Zify CstOp Op_bool_top.
 
 #[global]
-Instance Op_bool_top' : CstOp (Order.bottom : bool^d) := Op_true.
+Instance Op_bool_top' : CstOp (\bot : bool^d)%O := Op_true.
 Add Zify CstOp Op_bool_top'.
 
 #[global]
@@ -351,7 +351,7 @@ Instance Op_nat_join' : BinOp (Order.meet : nat^d -> _) := Op_maxn.
 Add Zify BinOp Op_nat_join'.
 
 #[global]
-Instance Op_nat_bottom : CstOp (Order.bottom : nat) := Op_O.
+Instance Op_nat_bottom : CstOp (\bot : nat)%O := Op_O.
 Add Zify CstOp Op_nat_bottom.
 
 (******************************************************************************)
@@ -578,20 +578,20 @@ Instance Op_natdvd_join' : BinOp (Order.meet : natdvd^d -> _) := Op_lcmn.
 Add Zify BinOp Op_natdvd_join'.
 
 #[global]
-Instance Op_natdvd_bottom : CstOp (Order.bottom : natdvd) :=
+Instance Op_natdvd_bottom : CstOp (\bot : natdvd)%O :=
   { TCst := 1%Z; TCstInj := erefl }.
 Add Zify CstOp Op_natdvd_bottom.
 
 #[global]
-Instance Op_natdvd_bottom' : CstOp (Order.top : natdvd^d) := Op_natdvd_bottom.
+Instance Op_natdvd_bottom' : CstOp (\top : natdvd^d)%O := Op_natdvd_bottom.
 Add Zify CstOp Op_natdvd_bottom'.
 
 #[global]
-Instance Op_natdvd_top : CstOp (Order.top : natdvd) := Op_O.
+Instance Op_natdvd_top : CstOp (\top : natdvd)%O := Op_O.
 Add Zify CstOp Op_natdvd_top.
 
 #[global]
-Instance Op_natdvd_top' : CstOp (Order.bottom : natdvd^d) := Op_O.
+Instance Op_natdvd_top' : CstOp (\bot : natdvd^d)%O := Op_O.
 Add Zify CstOp Op_natdvd_top'.
 
 Module Exports.