From 12edb9e2e5e4456a2fa89a62379dbbe02c842ed8 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 6 Aug 2024 12:37:55 +0200 Subject: [PATCH] fixes --- Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs | 3 +-- Source/DafnyCore/Dafny.atg | 5 ++--- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs index bac8247896..43e4aeeb79 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs @@ -455,8 +455,7 @@ public void PrintStatement(Statement stmt, int indent) { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement } - void PrintBy(ConcreteUpdateStatement s) - { + void PrintBy(ConcreteUpdateStatement s) { BlockStmt proof = s switch { UpdateStmt updateStmt => updateStmt.Proof, AssignOrReturnStmt returnStmt => returnStmt.Proof, diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 1571264c93..c226669085 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -2352,9 +2352,8 @@ UpdateStmt } ( "by" BlockStmt - | ";" - ) - ";" (. endTok = t; .) + | ";" (. endTok = t; .) + ) ) (. var rangeToken = new RangeToken(startToken, t); if (suchThat != null) {