Commit eb7a762b authored by Robbert Krebbers's avatar Robbert Krebbers

Change the Coq scope notations for viewshifts into parsing only.

They mess up the proof mode notations due to overlaps.
parent e4c96015
Pipeline #1240 passed with stage
......@@ -41,11 +41,9 @@ Notation "|==> Q" := (pvs ⊤ ⊤ Q%I)
(at level 99, Q at level 200, format "|==> Q") : uPred_scope.
Notation "P ={ E1 , E2 }=> Q" := (P |={E1,E2}=> Q)
(at level 99, E1, E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=> Q") : C_scope.
(at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
Notation "P ={ E }=> Q" := (P |={E}=> Q)
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=> Q") : C_scope.
(at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
Section pvs.
Context {Λ : language} {Σ : iFunctor}.
......
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