diff options
| author | Cyril Cohen | 2020-01-10 08:08:10 -0500 |
|---|---|---|
| committer | Cyril Cohen | 2020-01-10 08:08:10 -0500 |
| commit | 95ef2d5e5b38b2c091625b6309c536da0f4e0b0f (patch) | |
| tree | 9e4dc922f3493e73fc783e5b8520bdf046de050a | |
| parent | 941b90fd72a2c65218b063ce79de9b2a4bc5ae12 (diff) | |
Exporting T^d notation
| -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. |