diff --git a/opam b/opam
index d1175a57a9b4aa0a76dd4d30c1ac19fded8ceabc..203be2403f04a16beafe10bfbfef18e689c6434d 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 43454d356d152ac04bcf41f886534bc503381ed2..bfc7200d07911f36960d4da42d34e4f521fc1e5d 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 40aed8447af6daba0b1d95476708ecc33647a383..bab80a461290f7aee648f5607d64799acd46d78f 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.