From 5c3ad2f9bbc8471d27bc4e4fe72b4fb1f3f15391 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 25 Nov 2016 18:33:37 +0100
Subject: [PATCH] make the C-scope magic wand printing
---
base_logic/primitive.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index 27896d8d2..299d9cd30 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -190,7 +190,7 @@ Notation "P ==∗ Q" := (P -∗ |==> Q)%I
Coercion uPred_valid {M} (P : uPred M) : Prop := True%I ⊢ P.
Notation "P -∗ Q" := (P ⊢ Q)
- (at level 99, Q at level 200, right associativity, only parsing) : C_scope.
+ (at level 99, Q at level 200, right associativity) : C_scope.
Module uPred_primitive.
Definition unseal :=
--
GitLab