bump Iris

guix.scm

@@ -30,10 +30,10 @@
   #:use-module (gnu packages coq)
   #:use-module ((guix licenses) #:prefix license:))
 
-(define stdpp-commit "d98ab4e4adf80e34f2b38d95e125fa6d128e09e7")
-(define stdpp-sha256 (base32 "09dsdja35ls25h4dd842wiadhjjilazfl5kywn2vgrav4vzi3s5m")) ;; sha256 hash of the specific std++ checkout
-(define iris-commit "4760ad334dba7d4b683700e52ecb444b944daeed")
-(define iris-sha256 (base32 "0cxhjzbsl21w0vnl3ks826mba115xyg3bbxznirp42cwh4x24yxn")) ;; sha256 hash of the specific std++ checkout
+(define stdpp-commit "d6eb24f23eeb42529210a4d422392d7950d920c0")
+(define stdpp-sha256 (base32 "1m1ys10f16v5ndxmwfjnw43p0qdb6fkk08z8864357zwmpvf2vgg")) ;; sha256 hash of the specific std++ checkout
+(define iris-commit "a9031f7f4979974426c5c9fa4ac315863b99c362")
+(define iris-sha256 (base32 "05kmbljc68ndnl8jyn3xy14f3vhcbxq7n2n3bkjyyfiyl8b2vaql")) ;; sha256 hash of the specific std++ checkout
 (define %source-dir (dirname (current-filename)))
 
 (define-public coq-stdpp

opam

@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2019-04-07.4.4760ad33") | (= "dev") }
+  "coq-iris" { (= "dev.2019-04-25.1.a9031f7f") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]

theories/typing/types.v

@@ -87,11 +87,11 @@ unfold operator to be the identity function. *)
 Definition rec_unfold : val := λ: "x", "x".
 Definition unpack : val := λ: "x" "y", "y" "x".
 
-Notation "'unpack:' x := e1 'in' e2" := (unpack e1%E (Lam x%bind e2%E))
+Notation "'unpack:' x := e1 'in' e2" := (unpack e1%E (Lam x%binder e2%E))
   (at level 200, x at level 1, e1, e2 at level 200, only parsing,
    format "'[' 'unpack:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
 
-Notation "'unpack:' x := e1 'in' e2" := (unpack e1%E (LamV x%bind e2%E))
+Notation "'unpack:' x := e1 'in' e2" := (unpack e1%E (LamV x%binder e2%E))
   (at level 200, x at level 1, e1, e2 at level 200, only parsing,
    format "'[' 'unpack:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : val_scope.