diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-22 02:18:51 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-22 02:18:51 -0700 |
| commit | 2541e9de002267359897bf967755172fcc726512 (patch) | |
| tree | 43fcf2056a460973bb4619e2ac1d060343bd28bc /Source/Dafny/RefinementTransformer.cs | |
| parent | aba7928452a9043ab1cc6f4fd2e0dda4e2273508 (diff) | |
renamed "abstract module" to "module facade"
renamed "ghost module" to "abstract module", adding a keyword "abstract"
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 46cf156f..e1070dad 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -98,17 +98,17 @@ namespace Microsoft.Dafny if (d is ModuleDecl) {
if (!(nw is ModuleDecl)) {
reporter.Error(nw, "a module ({0}) must refine another module", nw.Name);
- } else if (!(d is AbstractModuleDecl)) {
- reporter.Error(nw, "a module ({0}) can only refine abstract modules", nw.Name);
+ } else if (!(d is ModuleFacadeDecl)) {
+ reporter.Error(nw, "a module ({0}) can only refine a module facade", nw.Name);
} else {
- ModuleSignature original = ((AbstractModuleDecl)d).OriginalSignature;
+ ModuleSignature original = ((ModuleFacadeDecl)d).OriginalSignature;
ModuleSignature derived = null;
if (nw is AliasModuleDecl) {
derived = ((AliasModuleDecl)nw).Signature;
- } else if (nw is AbstractModuleDecl) {
- derived = ((AbstractModuleDecl)nw).Signature;
+ } else if (nw is ModuleFacadeDecl) {
+ derived = ((ModuleFacadeDecl)nw).Signature;
} else {
- reporter.Error(nw, "a module ({0}) can only be refined by alias or abstract modules", d.Name);
+ reporter.Error(nw, "a module ({0}) can only be refined by an alias module or a module facade", d.Name);
}
if (derived != null) {
// check that the new module refines the previous declaration
|