diff options
author | qunyanm <unknown> | 2016-02-02 12:40:07 -0800 |
---|---|---|
committer | qunyanm <unknown> | 2016-02-02 12:40:07 -0800 |
commit | 2be514ca20e1478b6df02ef2b4c2725c319ac934 (patch) | |
tree | 87f0101c5a5c3f284cb81d2ccec706a60f321168 /Source | |
parent | e4da5fcd52bbdd0b8345056a3475333d6e27e65f (diff) |
Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B"
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Dafny/Dafny.atg | 2 | ||||
-rw-r--r-- | Source/Dafny/Parser.cs | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index e3696c5b..80792ce2 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -727,7 +727,7 @@ SubModuleDecl<DeclModifierData dmod, ModuleDefinition parent, out ModuleDecl sub (. submodule = new AliasModuleDecl(idPath, id, parent, opened); .)
| "as" QualifiedModuleName<out idPath> [IF(IsDefaultImport()) "default" QualifiedModuleName<out idAssignment> ]
(. submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened);
- //errors.Warning(t, "\"import A as B\" has been deprecated; in the new syntax, it is \"import A:B\"");
+ errors.Warning(t, "\"import A as B\" has been deprecated; in the new syntax, it is \"import A:B\"");
.)
| ":" QualifiedModuleName<out idPath>
(. submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); .)
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index c7955dc8..8a1da161 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -835,7 +835,7 @@ bool IsDefaultImport() { QualifiedModuleName(out idAssignment);
}
submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened);
- //errors.Warning(t, "\"import A as B\" has been deprecated; in the new syntax, it is \"import A:B\"");
+ errors.Warning(t, "\"import A as B\" has been deprecated; in the new syntax, it is \"import A:B\"");
} else if (la.kind == 21) {
Get();
|