Replace Order.bottom and Order.top with \bot and \top

math-comp · May 23, 2023 · 14224b1 · 14224b1
1 parent 1499da1
commit 14224b1
Showing 1 changed file with 9 additions and 9 deletions.
diff --git 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.