diff options
| -rw-r--r-- | mathcomp/ssreflect/order.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 29693d4..96cd9b9 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -2147,10 +2147,10 @@ Export FinTotal.Exports. Definition dual T : Type := T. Definition dual_display : unit -> unit. Proof. exact. Qed. -Local Notation "T ^d" := (dual T) (at level 2, format "T ^d") : type_scope. Module Import DualSyntax. +Notation "T ^d" := (dual T) (at level 2, format "T ^d") : type_scope. Notation "<=^d%O" := (@le (dual_display _) _) : fun_scope. Notation ">=^d%O" := (@ge (dual_display _) _) : fun_scope. Notation ">=^d%O" := (@ge (dual_display _) _) : fun_scope. |