From 64516f784a10a77b9a60771965bf5c33ac4570ef Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 28 Feb 2016 20:18:29 -0500 Subject: [PATCH] Fix goofy notation --- OperationalSemantics.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/OperationalSemantics.v b/OperationalSemantics.v index 04a78f8..a34ea6d 100644 --- a/OperationalSemantics.v +++ b/OperationalSemantics.v @@ -37,7 +37,7 @@ Infix "*" := Times : arith_scope. Delimit Scope arith_scope with arith. Notation "x <- e" := (Assign x e%arith) (at level 75). Infix ";;" := Sequence (at level 76). (* This one changed slightly, to avoid parsing clashes. *) -Notation "'when' e 'loop' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0). +Notation "'when' e 'then' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0). Notation "'while' e 'loop' body 'done'" := (While e%arith body) (at level 75). (* Here's an adaptation of our factorial example from Chapter 3. *) @@ -974,7 +974,7 @@ Module Concurrent. Notation "x <- e" := (Assign x e%arith) (at level 75). Infix ";;" := Sequence (at level 76). (* This one changed slightly, to avoid parsing clashes. *) - Notation "'when' e 'loop' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0). + Notation "'when' e 'then' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0). Notation "'while' e 'loop' body 'done'" := (While e%arith body) (at level 75). Infix "||" := Parallel.