From b76f8a0e1a7174b266aa64f82b08631a2efa5d10 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Tue, 17 Jul 2012 18:27:03 -0700
Subject: Dafny: allowed strictly finite datatypes in comprehensions,
 quantifiers, and parallel statements.

---
 Dafny/Resolver.cs | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'Dafny/Resolver.cs')

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 74ddb08b..8c14cb0c 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -4946,6 +4946,8 @@ namespace Microsoft.Dafny
         if (bv.Type is BoolType) {
           // easy
           bounds.Add(new QuantifierExpr.BoolBoundedPool());
+        } else if (bv.Type.IsIndDatatype && (bv.Type.AsIndDatatype).HasFinitePossibleValues) {
+          bounds.Add(new QuantifierExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));
         } else {
           // Go through the conjuncts of the range expression to look for bounds.
           Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;
-- 
cgit v1.2.3