Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that

the auto-triggers can be computed for ForallStmt.

1 files changed, 1 insertions, 0 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 847617aa..4c1e2bd7 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -4693,6 +4693,7 @@ namespace Microsoft.Dafny {
     public readonly Expression Range;

     public readonly List<MaybeFreeExpression> Ens;

     public readonly Statement Body;

+    public List<Expression> ForallExpressions;   // fill in by rewriter.

 

     public List<ComprehensionExpr.BoundedPool> Bounds;  // initialized and filled in by resolver

     // invariant: if successfully resolved, Bounds.Count == BoundVars.Count;