diff options
Diffstat (limited to 'mathcomp/ssreflect/order.v')
| -rw-r--r-- | mathcomp/ssreflect/order.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 1546a55..7cd178d 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -407,6 +407,9 @@ Set Implicit Arguments. 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. |