From 6398bd0f46ed66790d193a4dbcde3e2c0314b833 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 8 Feb 2016 18:58:34 -0800
Subject: Renamed identifiers for increased geopolitical appeal

---
 Test/dafny0/ResolutionErrors.dfy                   | 24 +++++++++++-----------
 Test/dafny0/ResolutionErrors.dfy.expect            |  6 +++---
 .../some-proofs-only-work-without-autoTriggers.dfy |  2 +-
 3 files changed, 16 insertions(+), 16 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)
diff --git a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy
index 98cea392..bc2e0934 100644
--- a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy
+++ b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy
@@ -1,7 +1,7 @@
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-// The examples below work nicely with /autoTriggers:0, but break when we ass
+// The examples below work nicely with /autoTriggers:0, but break when we use
 // /autoTriggers.
 
 // The issue is that the axioms for sequences are missing a number of facts,
-- 
cgit v1.2.3