2 files changed, 15 insertions, 15 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 58ba6701..8dceb6ba 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -459,7 +459,7 @@ module MyOwnModule {
   
 // ------------------- nameless constructors ------------------------------
 
-class YHWH {
+class Y {
   var data: int;
   constructor (x: int)
     modifies this;
@@ -470,22 +470,22 @@ class YHWH {
   {
   }
   method Test() {
-    var IAmWhoIAm := new YHWH(5);
-    IAmWhoIAm := new YHWH._ctor(7);  // but, in fact, it is also possible to use the underlying name
-    IAmWhoIAm := new YHWH;  // error: the class has a constructor, so one must be used
-    var s := new Lucifer.Init(5);
-    s := new Lucifer.FromArray(null);
-    s := new Lucifer(false);
-    s := new Lucifer._ctor(false);
-    s := new Lucifer.M();  // error: there is a constructor, so one must be called
-    s := new Lucifer;  // error: there is a constructor, so one must be called
+    var i := new Y(5);
+    i := new Y._ctor(7);  // but, in fact, it is also possible to use the underlying name
+    i := new Y;  // error: the class has a constructor, so one must be used
+    var s := new Luci.Init(5);
+    s := new Luci.FromArray(null);
+    s := new Luci(false);
+    s := new Luci._ctor(false);
+    s := new Luci.M();  // error: there is a constructor, so one must be called
+    s := new Luci;  // error: there is a constructor, so one must be called
     var l := new Lamb;
     l := new Lamb();  // error: there is no default constructor
     l := new Lamb.Gwen();
   }
 }
 
-class Lucifer {
+class Luci {
   constructor Init(y: int) { }
   constructor (nameless: bool) { }
   constructor FromArray(a: array<int>) { }
@@ -493,7 +493,7 @@ class Lucifer {
 }
 
 class Lamb {
-  method Jesus() { }
+  method Jess() { }
   method Gwen() { }
 }
 
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index b055184f..d1d826f4 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -173,9 +173,9 @@ ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype construc
 ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
 ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
 ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
-ResolutionErrors.dfy(475,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
-ResolutionErrors.dfy(480,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
-ResolutionErrors.dfy(481,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
+ResolutionErrors.dfy(475,6): Error: when allocating an object of type 'Y', one of its constructor methods must be called
+ResolutionErrors.dfy(480,6): Error: when allocating an object of type 'Luci', one of its constructor methods must be called
+ResolutionErrors.dfy(481,6): Error: when allocating an object of type 'Luci', one of its constructor methods must be called
 ResolutionErrors.dfy(483,9): Error: class Lamb does not have an anonymous constructor
 ResolutionErrors.dfy(853,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
 ResolutionErrors.dfy(857,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)