Dafny: improved error location for violations of function postconditions

1 files changed, 1 insertions, 1 deletions

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index d99ffdc9..280227f1 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -88,7 +88,7 @@ module SomeBody refines BodyFree {
 
 module FullBodied refines BodyFree {
   function F(x: int): int
-  { x } // error: does not meet the inherited postcondition (note, confusing error-message location)
+  { x } // error: does not meet the inherited postcondition
   method M() returns (a: int, b: int)
   {  // error: does not establish postcondition
     a := b + 1;