Skip to content

Commit

Permalink
Final strokes?
Browse files Browse the repository at this point in the history
  • Loading branch information
aterga committed Jan 4, 2023
1 parent 2f209e4 commit c0fd8bb
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion src/lowering/desugar.ml
Original file line number Diff line number Diff line change
Expand Up @@ -202,7 +202,7 @@ and exp' at note = function
| S.AndE (e1, e2) -> (andE (exp e1) (exp e2)).it
| S.OrE (e1, e2) -> (orE (exp e1) (exp e2)).it
| S.ImpliesE (e1, e2) -> (impliesE (exp e1) (exp e2)).it
| S.OldE (e) -> (oldE (exp e)).it
| S.OldE e -> (oldE (exp e)).it
| S.IfE (e1, e2, e3) -> I.IfE (exp e1, exp e2, exp e3)
| S.SwitchE (e1, cs) -> I.SwitchE (exp e1, cases cs)
| S.TryE (e1, cs) -> I.TryE (exp e1, cases cs)
Expand Down
2 changes: 1 addition & 1 deletion src/mo_def/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ module Make (Cfg : Config) = struct
| AndE (e1, e2) -> "AndE" $$ [exp e1; exp e2]
| OrE (e1, e2) -> "OrE" $$ [exp e1; exp e2]
| ImpliesE (e1, e2) -> "ImpliesE"$$ [exp e1; exp e2]
| OldE (e) -> "OldE" $$ [exp e]
| OldE e -> "OldE" $$ [exp e]
| IfE (e1, e2, e3) -> "IfE" $$ [exp e1; exp e2; exp e3]
| SwitchE (e, cs) -> "SwitchE" $$ [exp e] @ List.map case cs
| WhileE (e1, e2) -> "WhileE" $$ [exp e1; exp e2]
Expand Down
2 changes: 1 addition & 1 deletion src/mo_frontend/assertions.mly
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,6 @@ let is_verification () =
| ASSERT COLON s=NAT COLON ASYNC e=exp_nest
{ is_verification () &&& AssertE(Concurrency s, e) @? at $sloc }
| OLD e=exp_nest
{ is_verification () &&& OldE(e) @? at $sloc }
{ is_verification () &&& OldE e @? at $sloc }

%%

0 comments on commit c0fd8bb

Please sign in to comment.