From 2de8494a578909cdbc271391bf4b75b2f08bc375 Mon Sep 17 00:00:00 2001 From: Dan Frumin <dfrumin@cs.ru.nl> Date: Mon, 8 Apr 2019 09:16:06 +0200 Subject: [PATCH] bump Iris --- guix.scm | 4 ++-- opam | 2 +- theories/typing/types.v | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/guix.scm b/guix.scm index 821c451..48f35f8 100644 --- a/guix.scm +++ b/guix.scm @@ -32,8 +32,8 @@ (define stdpp-commit "d98ab4e4adf80e34f2b38d95e125fa6d128e09e7") (define stdpp-sha256 (base32 "09dsdja35ls25h4dd842wiadhjjilazfl5kywn2vgrav4vzi3s5m")) ;; sha256 hash of the specific std++ checkout -(define iris-commit "0495f1197f506ee13dacc242ebefda2f880951c9") -(define iris-sha256 (base32 "185vjm2sir3765g2c0f9d62mpv8dvl34sblqdh71x2g8cz0hiwzc")) ;; sha256 hash of the specific std++ checkout +(define iris-commit "4760ad334dba7d4b683700e52ecb444b944daeed") +(define iris-sha256 (base32 "0cxhjzbsl21w0vnl3ks826mba115xyg3bbxznirp42cwh4x24yxn")) ;; sha256 hash of the specific std++ checkout (define %source-dir (dirname (current-filename))) (define-public coq-stdpp diff --git a/opam b/opam index b410767..af2168f 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-03-26.0.0495f119") | (= "dev") } + "coq-iris" { (= "dev.2019-04-07.4.4760ad33") | (= "dev") } "coq-autosubst" { = "dev.coq86" } ] diff --git a/theories/typing/types.v b/theories/typing/types.v index af8a9c6..28347dd 100644 --- a/theories/typing/types.v +++ b/theories/typing/types.v @@ -68,7 +68,7 @@ Notation "∀: τ" := Notation "∃: τ" := (TExists τ%ty) (at level 100, τ at level 200) : FType_scope. -Notation "'ref' τ" := (Tref τ%ty) (at level 30, right associativity): FType_scope. +Notation "'ref' τ" := (Tref τ%ty) (at level 10, τ at next level, right associativity): FType_scope. (** * Typing judgements *) Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level). -- GitLab