From 2d44c0ef7cfa41be6f2884576f9f12c2023d0857 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 19 Jul 2016 22:41:28 +0200 Subject: [PATCH] Remove weird notation for par. --- heap_lang/lib/par.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v index cbd34ceb3..3e3ad7051 100644 --- a/heap_lang/lib/par.v +++ b/heap_lang/lib/par.v @@ -8,8 +8,7 @@ Definition par : val := let: "v2" := Snd "fs" #() in let: "v1" := join "handle" in Pair "v1" "v2". -Notation Par e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E. -Infix "||" := Par : expr_scope. +Notation "e1 || e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope. Global Opaque par. Section proof. -- GitLab