From 4a38c24a070c7c833e8e0678c5ebde542dd3d510 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 10 Oct 2020 12:47:27 +0200
Subject: [PATCH] update dependencies
---
opam | 2 +-
theories/lang/arc.v | 6 +++---
theories/lang/notation.v | 2 +-
3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/opam b/opam
index d1175a57..203be240 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2020-10-05.0.0974bf5a") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2020-10-10.1.4e05b3e8") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 43454d35..bfc7200d 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -2157,7 +2157,7 @@ Section arc.
case (decide (n = 1%positive)) => nEq.
- subst n. simpl in Eq'. subst q'. iSplitR "SA"; last first.
{ iExists None. by iFrame "SA". }
- iSplitL "SMA"; [by iExists _|]. simpl. rewrite frac_op' Eq''.
+ iSplitL "SMA"; [by iExists _|]. simpl. rewrite Eq''.
iDestruct "SeenM" as (t5 v5) "[#R5 MAX]". iDestruct "MAX" as %MAX.
iDestruct (GPS_SWSharedWriter_latest_time_1 with "W' R5") as %Le5.
iDestruct (GPS_SWSharedReader_Reader with "R'") as "#RR".
@@ -2332,7 +2332,7 @@ Section arc.
iCombine "SeenD" "SeenD'" as "SeenD'".
iDestruct (SeenActs_join with "SeenD'") as "SeenD'".
iSplitR "SA"; last first. { iExists None. by iFrame "SA". }
- iSplitL "SMA"; [by iExists _|]. rewrite frac_op' Eq''.
+ iSplitL "SMA"; [by iExists _|]. rewrite Eq''.
iDestruct "SeenM" as (t5 v5) "[#R5 MAX]". iDestruct "MAX" as %MAX.
iDestruct (GPS_SWSharedWriter_latest_time_1 with "W' R5") as %Le5.
iDestruct (GPS_SWSharedReader_Reader with "R'") as "#RR".
@@ -2716,7 +2716,7 @@ Section arc.
iDestruct (StrDowns_join with "[$SD $SD']") as "SD".
iCombine "SeenD" "SeenD'" as "SeenD'". iClear "SeenD".
iDestruct (SeenActs_join with "SeenD'") as "SeenD".
- rewrite HPn frac_op' Eq.
+ rewrite HPn Eq.
iAssert (SeenActs γs l (Mt ∪ {[t']}))%I with "[SW MAX]" as "#SeenM".
{ iExists _, _. iDestruct (GPS_SWWriter_Reader with "SW") as "$".
by iFrame "MAX". } iClear "rTrue R MAX". clear Vb MAX t2 v2 t v.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 40aed844..bab80a46 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -26,6 +26,6 @@ Notation "'letcall:' x := f args 'in' e" :=
we would even want them to print in general.
TODO: Introduce a Definition. *)
Notation "e1 '<-{Σ' i } '()'" := (e1 <- #i)%E
- (only parsing, at level 80, format "e1 <-{Σ i } ()" ) : expr_scope.
+ (only parsing, at level 80) : expr_scope.
Notation "e1 '<-{Σ' i } e2" := (e1 <-{Σ i} () ;; e1+ₗ#1 <- e2)%E
(at level 80, format "e1 <-{Σ i } e2") : expr_scope.
--
GitLab