diff options
| author |  Jason Koenig <unknown> | 2012-07-30 17:22:28 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-07-30 17:22:28 -0700 |
| commit | c3f4fae804fe07942cc1f0e4fc6e40b2542de645 (patch) | |
| tree | ec5ddee8d2d2fa8c520cfe8c7bef199e187d0100 /Test/dafny0/Answer | |
| parent | e9534ceb03a09e5524709a6f9112d8c7fb1df711 (diff) | |
Dafny: support opening modules into the local scope
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 8 |
1 files changed, 8 insertions, 0 deletions
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:
|