From 7da5e73bfd59e10d5271e25d06dcd04667bd00b5 Mon Sep 17 00:00:00 2001 From: Eric Giovannini <ecg19@seas.upenn.edu> Date: Tue, 14 Nov 2023 16:23:23 -0500 Subject: [PATCH] more fixes after updating cubical library --- formalizations/guarded-cubical/Common/Poset/Constructions.agda | 2 +- .../guarded-cubical/Common/Poset/MonotoneRelation.agda | 2 +- .../guarded-cubical/Semantics/LockStepErrorOrdering.agda | 2 +- .../guarded-cubical/Semantics/PredomainInternalHom.agda | 2 +- formalizations/guarded-cubical/Semantics/Predomains.agda | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/formalizations/guarded-cubical/Common/Poset/Constructions.agda b/formalizations/guarded-cubical/Common/Poset/Constructions.agda index 3aae364..ca4b0be 100644 --- 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) diff --git a/formalizations/guarded-cubical/Common/Poset/MonotoneRelation.agda b/formalizations/guarded-cubical/Common/Poset/MonotoneRelation.agda index 17693fe..3c628db 100644 --- 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 diff --git a/formalizations/guarded-cubical/Semantics/LockStepErrorOrdering.agda b/formalizations/guarded-cubical/Semantics/LockStepErrorOrdering.agda index 99c31f0..c37daff 100644 --- 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 diff --git a/formalizations/guarded-cubical/Semantics/PredomainInternalHom.agda b/formalizations/guarded-cubical/Semantics/PredomainInternalHom.agda index e41411c..b7e0d5c 100644 --- 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 diff --git a/formalizations/guarded-cubical/Semantics/Predomains.agda b/formalizations/guarded-cubical/Semantics/Predomains.agda index 77de44b..dbc948b 100644 --- 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) -- GitLab