From 5662c7f93cdb4ad3e43c89ee72d08b037ce6e890 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 20 Nov 2020 01:01:22 +0100
Subject: Removing unused cpo_sort scope

---
 mathcomp/ssreflect/order.v | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 7cd178d..f40c1d5 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -408,7 +408,6 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Declare Scope order_scope.
-Declare Scope cpo_sort.
 
 Delimit Scope order_scope with O.
 Local Open Scope order_scope.
@@ -1057,7 +1056,6 @@ End Exports.
 
 End POrder.
 Import POrder.Exports.
-Bind Scope cpo_sort with POrder.sort.
 
 Section POrderDef.
 
@@ -2072,7 +2070,6 @@ End Exports.
 
 End FinPOrder.
 Import FinPOrder.Exports.
-Bind Scope cpo_sort with FinPOrder.sort.
 
 Module FinLattice.
 Section ClassDef.
-- 
cgit v1.2.3