Commit 5c3ad2f9 authored by Ralf Jung's avatar Ralf Jung

make the C-scope magic wand printing

parent add4702b
Pipeline #3129 passed with stage
in 10 minutes and 28 seconds
......@@ -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 :=
......
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