summaryrefslogtreecommitdiff
path: root/Test/hofs
diff options
context:
space:
mode:
authorGravatar leino <unknown>2014-10-28 17:44:39 -0700
committerGravatar leino <unknown>2014-10-28 17:44:39 -0700
commit655b8311917e38cc2b359bad46def21de7852508 (patch)
tree8c7881bac939013d25a28e82e9860c456f034ea0 /Test/hofs
parent6c9a50e81dbdb791c558ac0a3463f01ee6a7f580 (diff)
Disallow automatic completion of type arguments to the LHS of datatype declarations
Diffstat (limited to 'Test/hofs')
-rw-r--r--Test/hofs/Fold.dfy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/hofs/Fold.dfy b/Test/hofs/Fold.dfy
index 7ce99e56..50b5569b 100644
--- a/Test/hofs/Fold.dfy
+++ b/Test/hofs/Fold.dfy
@@ -1,7 +1,7 @@
// RUN: %dafny /compile:3 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-datatype List = Nil | Cons(A,List<A>);
+datatype List<A> = Nil | Cons(A,List<A>);
datatype Expr = Add(List<Expr>) | Mul(List<Expr>) | Lit(int);