diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-12-07 16:49:25 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-12-07 16:49:25 -0800 |
| commit | aac18123c659a20aedb7cde57d87c59e01cf1d97 (patch) | |
| tree | e6beaf32f807fc4eebe5b431e18db129292e97b0 /Dafny/Compiler.cs | |
| parent | d8d1996a574c972b24216f9bfd922cc215df2668 (diff) | |
| parent | b3316fbe0671878a05378eaacba9951ab5565f55 (diff) | |
Merge
Diffstat (limited to 'Dafny/Compiler.cs')
| -rw-r--r-- | Dafny/Compiler.cs | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index b49c011f..78ea8d3d 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -74,7 +74,10 @@ namespace Microsoft.Dafny { }
foreach (TopLevelDecl d in m.TopLevelDecls) {
wr.WriteLine();
- if (d is DatatypeDecl) {
+ if (d is ArbitraryTypeDecl) {
+ var at = (ArbitraryTypeDecl)d;
+ Error("Arbitrary type ('{0}') cannot be compiled", at.Name);
+ } else if (d is DatatypeDecl) {
DatatypeDecl dt = (DatatypeDecl)d;
Indent(indent);
wr.Write("public abstract class Base_{0}", dt.Name);
|