diff options
| author |  chrishaw <unknown> | 2015-04-02 19:59:14 -0700 |
|---|---|---|
| committer | chrishaw <unknown> | 2015-04-02 19:59:14 -0700 |
| commit | 4d502277ed355fc739cf0c1856044c30645fcd13 (patch) | |
| tree | 67d4b59eb4b1735e18119c87a8ce7b793f0d8ad3 /Source/Dafny/Dafny.atg | |
| parent | 8a332057c2c9fc76e5fb112d430404d1aa47ea0d (diff) | |
Eliminate redundant checks of newtype and opaque function well-formedness from included files
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index a9653439..56d8a431 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -737,8 +737,8 @@ NewtypeDecl<ModuleDefinition module, out TopLevelDecl td> NoUSIdent<out bvId>
[ ":" Type<out baseType> ] (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false); } .)
"|"
- Expression<out wh, false, true> (. td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)
- | Type<out baseType> (. td = new NewtypeDecl(id, id.val, module, baseType, attrs); .)
+ Expression<out wh, false, true> (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)
+ | Type<out baseType> (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); .)
)
.
OtherTypeDecl<ModuleDefinition module, out TopLevelDecl td>
|