From d368258a234bd96859b434b9e320651630de9d8e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Tue, 4 Mar 2025 09:41:50 +0100
Subject: [PATCH] bump iris
---
semantics.opam | 2 +-
.../program_logics/program_logic/notation.v | 17 ++++++++---------
2 files changed, 9 insertions(+), 10 deletions(-)
diff --git a/semantics.opam b/semantics.opam
index 05534f2..54e76fd 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -10,7 +10,7 @@ version: "dev"
depends: [
"coq" { (>= "8.20" & < "8.21~") | (= "dev") }
- "coq-iris-heap-lang" { (= "dev.2024-12-06.1.72e683c9") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2025-02-27.1.c773500a") | (= "dev") }
"coq-equations" { (= "1.3.1+8.20") }
"coq-autosubst" { (= "1.9") | (= "dev") }
]
diff --git a/theories/program_logics/program_logic/notation.v b/theories/program_logics/program_logic/notation.v
index 88b1855..5f32211 100644
--- a/theories/program_logics/program_logic/notation.v
+++ b/theories/program_logics/program_logic/notation.v
@@ -43,27 +43,26 @@ Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ ⊤ e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e @ s ; E1 ; E2 {{ v , Q } }" := (wp s E1 E2 e%E (λ v, Q))
- (at level 20, e, Q at level 200,
+ (at level 20, e, Q at level 200, v at level 200 as pattern,
format "'[hv' 'WP' e '/' @ '[' s ; '/' E1 ; '/' E2 ']' '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
Notation "'WP' e @ E1 ; E2 {{ v , Q } }" := (wp NotStuck E1 E2 e%E (λ v, Q))
- (at level 20, e, Q at level 200,
+ (at level 20, e, Q at level 200, v at level 200 as pattern,
format "'[hv' 'WP' e '/' @ '[' E1 ; '/' E2 ']' '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
Notation "'WP' e @ E1 ; E2 ? {{ v , Q } }" := (wp MaybeStuck E1 E2 e%E (λ v, Q))
- (at level 20, e, Q at level 200,
+ (at level 20, e, Q at level 200, v at level 200 as pattern,
format "'[hv' 'WP' e '/' @ '[' E1 ; '/' E2 ']' '/' ? {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E E e%E (λ v, Q))
- (at level 20, e, Q at level 200,
+ (at level 20, e, Q at level 200, v at level 200 as pattern,
format "'[hv' 'WP' e '/' @ '[' s ; '/' E ']' '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck E E e%E (λ v, Q))
- (at level 20, e, Q at level 200,
+ (at level 20, e, Q at level 200, v at level 200 as pattern,
format "'[hv' 'WP' e '/' @ E '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
Notation "'WP' e @ E ? {{ v , Q } }" := (wp MaybeStuck E E e%E (λ v, Q))
- (at level 20, e, Q at level 200,
+ (at level 20, e, Q at level 200, v at level 200 as pattern,
format "'[hv' 'WP' e '/' @ E '/' ? {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
Notation "'WP' e {{ v , Q } }" := (wp NotStuck ⊤ ⊤ e%E (λ v, Q))
- (at level 20, e, Q at level 200,
+ (at level 20, e, Q at level 200, v at level 200 as pattern,
format "'[hv' 'WP' e '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
Notation "'WP' e ? {{ v , Q } }" := (wp MaybeStuck ⊤ ⊤ e%E (λ v, Q))
- (at level 20, e, Q at level 200,
+ (at level 20, e, Q at level 200, v at level 200 as pattern,
format "'[hv' 'WP' e '/' ? {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
-
--
GitLab