diff options
| author |  leino <unknown> | 2014-10-28 17:44:39 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-28 17:44:39 -0700 |
| commit | 655b8311917e38cc2b359bad46def21de7852508 (patch) | |
| tree | 8c7881bac939013d25a28e82e9860c456f034ea0 /Source | |
| parent | 6c9a50e81dbdb791c558ac0a3463f01ee6a7f580 (diff) | |
Disallow automatic completion of type arguments to the LHS of datatype declarations
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a44491de..01ef0a4b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3399,12 +3399,11 @@ namespace Microsoft.Dafny Contract.Requires(ctor != null);
Contract.Requires(ctor.EnclosingDatatype != null);
Contract.Requires(dtTypeArguments != null);
- ResolveTypeOption option = dtTypeArguments.Count == 0 ? new ResolveTypeOption(ctor) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix);
foreach (Formal p in ctor.Formals) {
// In the following, we pass in a NoContext, because any cycle formed by newtype constraints would have to
// involve a non-null object in order to get to the field and its type, and there is no way in a newtype constraint
// to obtain a non-null object.
- ResolveType(p.tok, p.Type, new NoContext(ctor.EnclosingDatatype.Module), option, dtTypeArguments);
+ ResolveType(p.tok, p.Type, new NoContext(ctor.EnclosingDatatype.Module), ResolveTypeOptionEnum.AllowPrefix, dtTypeArguments);
}
}
@@ -3894,7 +3893,7 @@ namespace Microsoft.Dafny t.ResolvedClass = dd;
} else {
// d is a class or datatype, and it may have type parameters
- what = "class/datatype";
+ what = isArrow ? "function type" : "class/datatype";
t.ResolvedClass = d;
}
if (option.Opt == ResolveTypeOptionEnum.DontInfer) {
|