summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2016-02-02 12:40:07 -0800
committerGravatar qunyanm <unknown>2016-02-02 12:40:07 -0800
commit2be514ca20e1478b6df02ef2b4c2725c319ac934 (patch)
tree87f0101c5a5c3f284cb81d2ccec706a60f321168 /Source
parente4da5fcd52bbdd0b8345056a3475333d6e27e65f (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.atg2
-rw-r--r--Source/Dafny/Parser.cs2
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();