From d185a08caf0ffb03918e461933a86268289bf56d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 4 Nov 2017 14:35:08 +0100
Subject: [PATCH] Bump Iris.

---
 opam                    |  2 +-
 theories/lang/tactics.v | 14 ++++++--------
 2 files changed, 7 insertions(+), 9 deletions(-)

diff --git a/opam b/opam
index ac688b5a..d80a8a36 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2017-11-02.0") | (= "dev") }
+  "coq-iris" { (= "dev.2017-11-04.0") | (= "dev") }
 ]
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index a4a69dbf..e890b488 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -144,7 +144,7 @@ Proof.
   - induction el=>//=. f_equal; auto.
 Qed.
 
-Definition atomic (e: expr) : bool :=
+Definition is_atomic (e: expr) : bool :=
   match e with
   | Read (ScOrd | Na2Ord) e | Alloc e => bool_decide (is_Some (to_val e))
   | Write (ScOrd | Na2Ord) e1 e2 | Free e1 e2 =>
@@ -153,7 +153,7 @@ Definition atomic (e: expr) : bool :=
     bool_decide (is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2))
   | _ => false
   end.
-Lemma atomic_correct e : atomic e → language.atomic (to_expr e).
+Lemma is_atomic_correct e : is_atomic e → Atomic (to_expr e).
 Proof.
   intros He. apply ectx_language_atomic.
   - intros σ e' σ' ef.
@@ -195,13 +195,11 @@ Hint Extern 10 (AsVal _) => solve_to_val : typeclass_instances.
 
 Ltac solve_atomic :=
   match goal with
-  | |- language.atomic ?e =>
-     let e' := W.of_expr e in change (language.atomic (W.to_expr e'));
-     apply W.atomic_correct; vm_compute; exact I
+  | |- Atomic ?e =>
+     let e' := W.of_expr e in change (Atomic (W.to_expr e'));
+     apply W.is_atomic_correct; vm_compute; exact I
   end.
-Hint Extern 0 (language.atomic _) => solve_atomic.
-(* For the side-condition of elim_vs_pvs_wp_atomic *)
-Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances.
+Hint Extern 0 (Atomic _) => solve_atomic : typeclass_instances.
 
 (** Substitution *)
 Ltac simpl_subst :=
-- 
GitLab