From c3f4fae804fe07942cc1f0e4fc6e40b2542de645 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Mon, 30 Jul 2012 17:22:28 -0700
Subject: Dafny: support opening modules into the local scope

---
 Test/dafny0/Answer | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'Test/dafny0/Answer')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index e3246f8f..3899b6df 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -757,6 +757,14 @@ Execution trace:
 
 Dafny program verifier finished with 22 verified, 5 errors
 
+-------------------- Modules2.dfy --------------------
+Modules2.dfy(44,17): Error: The name C ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)
+Modules2.dfy(44,10): Error: new can be applied only to reference types (got C)
+Modules2.dfy(47,14): Error: the name 'E' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'D.E')
+Modules2.dfy(48,14): Error: The name D ambiguously refers to a type in one of the modules A, B
+Modules2.dfy(50,11): Error: The name f ambiguously refers to a static member in one of the modules A, B
+5 resolution/type errors detected in Modules2.dfy
+
 -------------------- BadFunction.dfy --------------------
 BadFunction.dfy(6,3): Error: failure to decrease termination measure
 Execution trace:
-- 
cgit v1.2.3