From d2147936d579ca84b3b4dcfab0bb54aa4dc96e53 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 18 Jun 2018 15:54:02 +0200 Subject: [PATCH] backport heap_lang notation fix from gen_proofmode --- theories/heap_lang/lang.v | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v index e4e5dc55a..31b9b4c7f 100644 --- a/theories/heap_lang/lang.v +++ b/theories/heap_lang/lang.v @@ -531,11 +531,12 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang. Export heap_lang. (** Define some derived forms *) -Notation Lam x e := (Rec BAnon x e). -Notation Let x e1 e2 := (App (Lam x e2) e1). -Notation Seq e1 e2 := (Let BAnon e1 e2). -Notation LamV x e := (RecV BAnon x e). -Notation LetCtx x e2 := (AppRCtx (LamV x e2)). -Notation SeqCtx e2 := (LetCtx BAnon e2). +Notation Lam x e := (Rec BAnon x e) (only parsing). +Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing). +Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing). +Notation LamV x e := (RecV BAnon x e) (only parsing). +Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing). +Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing). +Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing). + Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)). -Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)). -- GitLab