From dbd3fa01b35eddce78214daed942a1af300b111c Mon Sep 17 00:00:00 2001 From: Dan Frumin <dfrumin@cs.ru.nl> Date: Fri, 26 Apr 2019 10:57:23 +0200 Subject: [PATCH] bump Iris --- guix.scm | 8 ++++---- opam | 2 +- theories/typing/types.v | 4 ++-- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/guix.scm b/guix.scm index 48f35f8..e21e5a3 100644 --- a/guix.scm +++ b/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 diff --git a/opam b/opam index af2168f..b5e192c 100644 --- a/opam +++ b/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" } ] diff --git a/theories/typing/types.v b/theories/typing/types.v index 28347dd..6f97fbb 100644 --- a/theories/typing/types.v +++ b/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. -- GitLab