From 95ef2d5e5b38b2c091625b6309c536da0f4e0b0f Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 10 Jan 2020 08:08:10 -0500
Subject: Exporting T^d notation

---
 mathcomp/ssreflect/order.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

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.
-- 
cgit v1.2.3