more fixes after updating cubical library

7da5e73b · Eric Giovannini · 8122aca7 · 7da5e73b · 7da5e73b · 7da5e73b
Commit 7da5e73b authored 1 year ago by Eric Giovannini
--- a/formalizations/guarded-cubical/Common/Poset/Constructions.agda
+++ b/formalizations/guarded-cubical/Common/Poset/Constructions.agda
@@ -8,7 +8,7 @@ module Common.Poset.Constructions where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
 open import Cubical.Relation.Binary
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Bool
 open import Cubical.Data.Nat renaming (ℕ to Nat)

--- a/formalizations/guarded-cubical/Common/Poset/MonotoneRelation.agda
+++ b/formalizations/guarded-cubical/Common/Poset/MonotoneRelation.agda
@@ -10,7 +10,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function

 open import Cubical.Relation.Binary
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 open import Cubical.Foundations.Structure
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.HLevels

--- a/formalizations/guarded-cubical/Semantics/LockStepErrorOrdering.agda
+++ b/formalizations/guarded-cubical/Semantics/LockStepErrorOrdering.agda
@@ -8,7 +8,7 @@ open import Common.Later
 module Semantics.LockStepErrorOrdering (k : Clock) where

 open import Cubical.Relation.Binary
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset

 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function

--- a/formalizations/guarded-cubical/Semantics/PredomainInternalHom.agda
+++ b/formalizations/guarded-cubical/Semantics/PredomainInternalHom.agda
@@ -7,7 +7,7 @@ module Semantics.PredomainInternalHom where

 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset


 open import Semantics.Predomains

--- a/formalizations/guarded-cubical/Semantics/Predomains.agda
+++ b/formalizations/guarded-cubical/Semantics/Predomains.agda
@@ -8,7 +8,7 @@ module Semantics.Predomains where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
 open import Cubical.Relation.Binary
-open import Cubical.Relation.Binary.Poset
+open import Cubical.Relation.Binary.Order.Poset
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Bool
 open import Cubical.Data.Nat renaming (ℕ to Nat)