Merge.

Changes that were needed included preventing the InductionRewriter from
iterating on a SplitQuantifier and using the new error reporting engine.

1 files changed, 1 insertions, 7 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index c969ac1f..c94f7836 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1201,13 +1201,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(targs));

       Contract.Ensures(Contract.Result<string>() != null);

 

-      string s = "";

-      string sep = "";

-      foreach (TypeParameter tp in targs) {

-        s += sep + "@" + tp.CompileName;

-        sep = ",";

-      }

-      return s;

+      return Util.Comma(targs, tp => "@" + tp.CompileName);

     }

 

     string DefaultValue(Type type)