Commit 6ca91820 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 8d0a7e56 ef4c1dca
......@@ -35,9 +35,15 @@ Notation "P ={ E }=★ Q" := (P ⊢ |={E}=> Q)
Notation "|={ E1 , E2 }▷=> Q" := (|={E1,E2}=> ( |={E2,E1}=> Q))%I
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }▷=> Q") : uPred_scope.
Notation "P ={ E1 , E2 }▷=★ Q" := (P - |={ E1 , E2 }=> Q)%I
(at level 99, E1, E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }▷=★ Q") : uPred_scope.
Notation "|={ E }▷=> Q" := (|={E,E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "|={ E }▷=> Q") : uPred_scope.
Notation "P ={ E }▷=★ Q" := (P ={E,E}= Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }▷=★ Q") : uPred_scope.
Section fupd.
Context `{irisG Λ Σ}.
......
......@@ -20,13 +20,6 @@ Notation "P ={ E }=> Q" := (True ⊢ P ={E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=> Q") : C_scope.
Notation "P ={ E1 , E2 }▷=> Q" := (P ={E1,E2}=> |={E2,E1}=> Q)%I
(at level 99, E1, E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }▷=> Q") : uPred_scope.
Notation "P ={ E }▷=> Q" := (P ={E,E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }▷=> Q") : uPred_scope.
Section vs.
Context `{irisG Λ Σ}.
Implicit Types P Q R : iProp Σ.
......
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