From 6c83f2c8160fa80b8e760c3eeff0e22d44147523 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 30 Jan 2017 10:50:19 +0100
Subject: [PATCH] Forgot to add two files.

---
 opam.pins                                | 2 +-
 theories/typing/unsafe/refcell/refcell.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/opam.pins b/opam.pins
index 67879a59..642f2e56 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0379384d795a443cb5ea31354644244f97a3299d
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b0418bd57b9341dbf5e58669c689201daa561bd7
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/unsafe/refcell/refcell.v
index 65938cf2..e2df4a41 100644
--- a/theories/typing/unsafe/refcell/refcell.v
+++ b/theories/typing/unsafe/refcell/refcell.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Definition refcell_stR :=
-  optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) posR)).
+  optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) positiveR)).
 Class refcellG Σ :=
   RefCellG :> inG Σ (authR refcell_stR).
 
-- 
GitLab