Commit 194b69cd authored by Robbert Krebbers's avatar Robbert Krebbers

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

parents 43d45c6b d5dd9dd4
Pipeline #504 failed with stage
...@@ -11,8 +11,8 @@ Definition par {X} : expr X := ...@@ -11,8 +11,8 @@ Definition par {X} : expr X :=
Notation Par e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E. Notation Par e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
Infix "||" := Par : expr_scope. Infix "||" := Par : expr_scope.
Instance do_wexpr_assert {X Y} (H : X `included` Y) : WExpr H par par := _. Instance do_wexpr_par {X Y} (H : X `included` Y) : WExpr H par par := _.
Instance do_wsubst_assert {X Y} x es (H : X `included` x :: Y) : Instance do_wsubst_par {X Y} x es (H : X `included` x :: Y) :
WSubst x es H par par := do_wsubst_closed _ x es H _. WSubst x es H par par := do_wsubst_closed _ x es H _.
Typeclasses Opaque par. Typeclasses Opaque par.
......
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