Commit d5dd9dd4 authored by Ralf Jung's avatar Ralf Jung

par: fix names of instances

parent 4e2dfc4e
Pipeline #499 failed with stage
......@@ -11,8 +11,8 @@ Definition par {X} : expr X :=
Notation Par e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
Infix "||" := Par : expr_scope.
Instance do_wexpr_assert {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_wexpr_par {X Y} (H : X `included` Y) : WExpr H par par := _.
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 _.
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