From faba734368205f3b4bec04a2d2c3c1bc5f016ead Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Wed, 2 Dec 2020 08:52:21 +0100
Subject: [PATCH] Fix various things

---
 _CoqProject                      | 4 +++-
 iris/algebra/dfrac.v             | 6 ++++++
 iris/base_logic/lib/gen_heap.v   | 6 ------
 iris_heap_lang/lib/atomic_heap.v | 2 +-
 iris_heap_lang/lib/increment.v   | 4 ++--
 iris_heap_lang/primitive_laws.v  | 4 +---
 6 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 534926fad..88e2135fc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -9,7 +9,9 @@
 -Q iris/program_logic iris.program_logic
 -Q iris_heap_lang iris.heap_lang
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
--arg -w -arg -notation-overridden
+-arg -w -arg -notation-overridden 
+# Coq emits warnings when a custom entry is reimported, this is too noisy.
+-arg -w -arg -custom-entry-overriden
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index d3b668f05..768f688b8 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -32,6 +32,12 @@ Inductive dfrac :=
   | DfracDiscarded : dfrac
   | DfracBoth : Qp → dfrac.
 
+Declare Custom Entry dfrac.
+Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
+Notation "â–¡" := DfracDiscarded (in custom dfrac).
+Notation "{# q }" := (DfracOwn q) (in custom dfrac at level 1, q constr).
+Notation "" := (DfracOwn 1) (in custom dfrac).
+
 Section dfrac.
   Canonical Structure dfracO := leibnizO dfrac.
 
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 5df0215f5..cdee918d3 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -123,12 +123,6 @@ Section definitions.
 End definitions.
 Arguments meta {L _ _ V Σ _ A _ _} l N x.
 
-Declare Custom Entry dfrac.
-Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
-Notation "â–¡" := DfracDiscarded (in custom dfrac).
-Notation "{# q }" := (DfracOwn q) (in custom dfrac at level 1, q constr).
-Notation "" := (DfracOwn 1) (in custom dfrac).
-
 Local Notation "l ↦ dq v" := (mapsto l dq v)
   (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
 
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index f40d17bd7..106b37585 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -47,7 +47,7 @@ Arguments atomic_heap _ {_}.
 
 (** Notation for heap primitives, in a module so you can import it separately. *)
 Module notation.
-otation "l ↦ dq v" := (mapsto l dq v)
+Notation "l ↦ dq v" := (mapsto l dq v)
   (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
 
 Notation "'ref' e" := (alloc e) : expr_scope.
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index 80ac951ce..174257263 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -111,8 +111,8 @@ Section increment.
   (* TODO: Generalize to q and 1-q, based on some theory for a "maybe-mapsto"
      connective that works on [option Qp] (the type of 1-q). *)
   Lemma weak_incr_spec (l: loc) (v : Z) :
-    l ↦{#(1/2)} #v -∗
-    <<< ∀ (v' : Z), l ↦{#(1/2)} #v' >>>
+    l ↦{#1/2} #v -∗
+    <<< ∀ (v' : Z), l ↦{#1/2} #v' >>>
       weak_incr #l @ ⊤
     <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
   Proof.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 4d3c577a9..58c527caa 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -28,8 +28,6 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
 
 (** Since we use an [option val] instance of [gen_heap], we need to overwrite
 the notations.  That also helps for scopes and coercions. *)
-Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V))
-  (at level 20) : bi_scope.
 Notation "l ↦ dq v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V))
   (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
 
@@ -277,7 +275,7 @@ Qed.
 (** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
 value type being [option val]. *)
 
-Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝%Qp.
+Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝.
 Proof. apply mapsto_valid. Qed.
 Lemma mapsto_valid_2 l dq1 dq2 v1 v2 :
   l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
-- 
GitLab