summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-02-25 21:18:21 -0800
committerGravatar qadeer <unknown>2014-02-25 21:18:21 -0800
commit26ad6fa295ca0bfd264fb87eb644e22b34aeef5b (patch)
tree95f8f114494927e7e040c7f27de97bf70287e086 /Source
parent8ec5a109f0611555a082e412723539b32fe3324d (diff)
parentf0a22c6bf37e4aa6519f24eacd0232e00d99ff59 (diff)
Merge
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/Absy.cs4
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index b220b373..8018f07d 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2156,14 +2156,14 @@ namespace Microsoft.Boogie {
List<TypeVariable>/*!*/ quantifiedTypeVars = new List<TypeVariable>();
foreach (TypeVariable/*!*/ t in TypeParameters) {
Contract.Assert(t != null);
- quantifiedTypeVars.Add(new TypeVariable(Token.NoToken, t.Name));
+ quantifiedTypeVars.Add(new TypeVariable(tok, t.Name));
}
Expr call = new NAryExpr(tok, new FunctionCall(new IdentifierExpr(tok, Name)), callArgs);
// specify the type of the function, because it might be that
// type parameters only occur in the output type
call = Expr.CoerceType(tok, call, (Type)OutParams[0].TypedIdent.Type.Clone());
- Expr def = Expr.Eq(call, definition);
+ Expr def = Expr.Binary(tok, BinaryOperator.Opcode.Eq, call, definition);
if (quantifiedTypeVars.Count != 0 || dummies.Count != 0) {
def = new ForallExpr(tok, quantifiedTypeVars, dummies,
kv,