Skip to content

Commit 4ee13ab

Browse files
authored
fix bug Relation.Binary.Morphism.Bundles (#2713)
1 parent 6d018a3 commit 4ee13ab

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Relation/Binary/OrderMorphism.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ module Relation.Binary.OrderMorphism where
1111

1212
{-# WARNING_ON_IMPORT
1313
"Relation.Binary.OrderMorphism was deprecated in v1.5.
14-
Use Relation.Binary.Reasoning.Morphism instead."
14+
Use Relation.Binary.Morphism.Bundles instead."
1515
#-}
1616

1717
open import Relation.Binary.Core using (_=[_]⇒_)

0 commit comments

Comments
 (0)