diff options
Diffstat (limited to 'Dafny/RefinementTransformer.cs')
-rw-r--r-- | Dafny/RefinementTransformer.cs | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs index a25d1eb8..adf99859 100644 --- a/Dafny/RefinementTransformer.cs +++ b/Dafny/RefinementTransformer.cs @@ -104,11 +104,7 @@ namespace Microsoft.Dafny { } else if (nw is ArbitraryTypeDecl) {
reporter.Error(nw, "an arbitrary type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);
} else if (nw is DatatypeDecl) {
- if (d is ClassDecl) {
- reporter.Error(nw, "a datatype declaration ({0}) in a refining module cannot replace a class declaration in the refinement base", nw.Name);
- } else {
- m.TopLevelDecls[index] = MergeDatatype((DatatypeDecl)nw, (DatatypeDecl)d);
- }
+ reporter.Error(nw, "a datatype declaration ({0}) in a refinement module can only replace an arbitrary-type declaration", nw.Name);
} else {
Contract.Assert(nw is ClassDecl);
if (d is DatatypeDecl) {
@@ -502,11 +498,6 @@ namespace Microsoft.Dafny { // -------------------------------------------------- Merging ---------------------------------------------------------------
- DatatypeDecl MergeDatatype(DatatypeDecl nw, DatatypeDecl prev) {
- // TODO
- return nw;
- }
-
ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) {
// TODO
return nw;
|