Commit 45f84a82 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix notation for ndot.

The non applied one should be only parsing.
parent e9af95ac
Pipeline #77 passed with stage
......@@ -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.
......
......@@ -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.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment