fixed knock-on ambiguity bugs

agda · Oct 2, 2024 · deaf59e · deaf59e
1 parent 3923598
commit deaf59e
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda
@@ -395,4 +395,4 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
 
   open RawApartnessRelation rawApartnessRelation public
     hiding (Carrier; _≈_ ; _#_)
-  
+
diff --git a/src/Relation/Binary/Properties/Poset.agda b/src/Relation/Binary/Properties/Poset.agda
@@ -25,7 +25,7 @@ open Poset P renaming (Carrier to A)
 
 import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
 import Relation.Binary.Properties.Preorder preorder as PreorderProperties
-open Eq using (_≉_)
+
 
 ------------------------------------------------------------------------
 -- The _≥_ relation is also a poset.