summaryrefslogtreecommitdiff
path: root/Source/Dafny/RefinementTransformer.cs
diff options
context:
space:
mode:
authorGravatar leino <unknown>2014-08-26 05:38:28 -0700
committerGravatar leino <unknown>2014-08-26 05:38:28 -0700
commitf28472da56c5cb38c343bb1e1d8c791fbf22914f (patch)
treec6d197d8a82ab2d71cb71a19797a7b58fe89e728 /Source/Dafny/RefinementTransformer.cs
parentf7d1a3200a18cb15bc49f6d89068ddd1e99efe0e (diff)
Refactoring: renamed DerivedTypeDecl to NewtypeDecl
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
-rw-r--r--Source/Dafny/RefinementTransformer.cs4
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 69dfb03d..5f116779 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -163,10 +163,10 @@ namespace Microsoft.Dafny
if (nw.TypeArgs.Count != d.TypeArgs.Count) {
reporter.Error(nw, "opaque type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
}
- } else if (nw is DerivedTypeDecl) {
+ } else if (nw is NewtypeDecl) {
// fine, as long as "nw" does not take any type parameters
if (nw.TypeArgs.Count != 0) {
- reporter.Error(nw, "opaque type '{0}', which has {1} type argument{2}, is not allowed to be replaced by a derived type, which takes none", nw.Name, d.TypeArgs.Count, d.TypeArgs.Count == 1 ? "" : "s");
+ reporter.Error(nw, "opaque type '{0}', which has {1} type argument{2}, is not allowed to be replaced by a newtype, which takes none", nw.Name, d.TypeArgs.Count, d.TypeArgs.Count == 1 ? "" : "s");
}
} else if (nw is CoDatatypeDecl) {
reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");