From e10098cde7bac9a7a1576000fa29d15f1fcd8970 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 2 Jul 2015 16:06:02 -0700
Subject: Type parameters in method/function signatures are no longer
 auto-declared.  Although convenient and concise, the auto-declare behavior
 has on many occasions caused confusion when a type name has accidentally been
 mistyped (and Dafny had then accepted and auto-declared the name). Note, the
 behavior of filling in missing type parameters is still supported.  This
 mode, although unusual (even original?) in languages, is different from the
 auto- declare behavior.  For auto-declare, identifiers could be used in the
 program without having a declaration.  For fill-in parameters, the implicitly
 declared type parameters remain anonymous.

---
 Source/Dafny/Resolver.cs | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'Source/Dafny/Resolver.cs')

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 29e36ccd..7c78c1e2 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -8469,12 +8469,6 @@ namespace Microsoft.Dafny
           r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);
         }
 #endif
-      } else if (option.Opt == ResolveTypeOptionEnum.AllowPrefixExtend && expr.OptTypeArguments == null) {
-        // it woulc plausibly be a type parameter, but isn't; we will declare it automatically
-        tp = new TypeParameter(expr.tok, expr.Name, defaultTypeArguments.Count, option.Parent);
-        defaultTypeArguments.Add(tp);
-        r = new Resolver_IdentifierExpr(expr.tok, tp);
-        allTypeParameters.Push(expr.Name, tp);
       } else {
         // ----- None of the above
         Error(expr.tok, "Undeclared top-level type or type parameter: {0} (did you forget to qualify a name?)", expr.Name);
-- 
cgit v1.2.3