From 45f84a82299b72381f6c436dd77701d55e4dcbe9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 22 Feb 2016 22:33:56 +0100
Subject: [PATCH] Fix notation for ndot.

The non applied one should be only parsing.
---
 barrier/client.v           | 6 +++---
 program_logic/namespaces.v | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/barrier/client.v b/barrier/client.v
index 8ad1d8f26..5e888030c 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -33,13 +33,13 @@ Section ClosedProofs.
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
   Proof.
-    apply ht_alt. rewrite (heap_alloc ⊤ (ndot nroot "Barrier")); last first.
+    apply ht_alt. rewrite (heap_alloc ⊤ (nroot .: "Barrier")); last first.
     { (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
-      move=>? _. exact I. }
+      by move=>? _. }
     apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
     rewrite -(client_safe (nroot .: "Heap" ) (nroot .: "Barrier" )) //.
     (* This, too, should be automated. *)
-    apply ndot_ne_disjoint. discriminate.
+    by apply ndot_ne_disjoint.
   Qed.
 
   Print Assumptions client_safe_closed.
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 84ed58a5e..08a2c881d 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -8,7 +8,7 @@ Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
 Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
 
 Infix ".:" := ndot (at level 19, left associativity) : C_scope.
-Notation "(.:)" := ndot : C_scope.
+Notation "(.:)" := ndot (only parsing) : C_scope.
 
 Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
 Proof. by intros N1 x1 N2 x2 ?; simplify_eq. Qed.
-- 
GitLab