Scope Cleanup

math-comp · Jan 21, 2024 · 9c63c85 · 9c63c85
1 parent 4ed52f3
commit 9c63c85
Showing 1 changed file with 7 additions and 4 deletions.
diff --git a/theories/SymGroup/weak_order.v b/theories/SymGroup/weak_order.v
@@ -40,6 +40,9 @@ Unset Printing Implicit Defensive.
 Import GroupScope.
 Import Order.Theory.
 
+#[local] Open Scope Combi_scope.
+
+
 Reserved Notation "s '<=R' t" (at level 70, t at next level).
 Reserved Notation "s '<R' t"  (at level 70, t at next level).
 Reserved Notation "s '/\R' t" (at level 70, t at next level).
@@ -107,10 +110,10 @@ End Def.
 Module Exports.
 HB.reexport WeakOrder.
 
-Notation "x <=R y" := (@Order.le perm_display _ (x : 'S__) y).
-Notation "x <R y" := (@Order.lt perm_display _ (x : 'S__) y).
-Notation "x /\R y" := (@Order.meet perm_display _ (x : 'S__) y).
-Notation "x \/R y" := (@Order.join perm_display _ (x : 'S__) y).
+Notation "x <=R y" := (@Order.le perm_display _ (x : 'S__) y) : Combi_scope.
+Notation "x <R y" := (@Order.lt perm_display _ (x : 'S__) y) : Combi_scope.
+Notation "x /\R y" := (@Order.meet perm_display _ (x : 'S__) y) : Combi_scope.
+Notation "x \/R y" := (@Order.join perm_display _ (x : 'S__) y) : Combi_scope.
 
 Section WeakOrder.