summaryrefslogtreecommitdiff
path: root/Test/dafny0/ResolutionErrors.dfy.expect
diff options
context:
space:
mode:
authorGravatar leino <unknown>2014-08-02 01:05:17 -0700
committerGravatar leino <unknown>2014-08-02 01:05:17 -0700
commitae578ae92040975fed005d045110679e4e858c31 (patch)
tree79f2a3a67c8c9059a89d9771e933c8a0b6b601bf /Test/dafny0/ResolutionErrors.dfy.expect
parent54b670417f5974c43ef2fd55d37ba3806ad5c72d (diff)
Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in the resolver and translator
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy.expect')
-rw-r--r--Test/dafny0/ResolutionErrors.dfy.expect3
1 files changed, 2 insertions, 1 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 49cfe650..d5d12eb9 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -63,6 +63,7 @@ ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter
ResolutionErrors.dfy(1000,7): Error: Cycle among type synonyms: A -> A
ResolutionErrors.dfy(1003,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1007,7): Error: Cycle among type synonyms: A -> B -> A
+ResolutionErrors.dfy(1016,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
ResolutionErrors.dfy(1019,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1024,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x
@@ -171,4 +172,4 @@ ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (i
ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real)
ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int)
ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)
-173 resolution/type errors detected in ResolutionErrors.dfy
+174 resolution/type errors detected in ResolutionErrors.dfy