From cb4f549f83d46a84c119b4c412b4c6aae64f153e Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 24 Apr 2017 12:54:47 -0400
Subject: Add loop invariant framework for for-loops

Also fix bugs in for-loop definition to make the proofs go through
---
 _CoqProject | 3 +++
 1 file changed, 3 insertions(+)

(limited to '_CoqProject')

diff --git a/_CoqProject b/_CoqProject
index b41e8f6b9..416165ad1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -248,7 +248,10 @@ src/Util/Unit.v
 src/Util/WordUtil.v
 src/Util/ZRange.v
 src/Util/ZUtil.v
+src/Util/ForLoop/Instances.v
+src/Util/ForLoop/InvariantFramework.v
 src/Util/ForLoop/Tests.v
+src/Util/ForLoop/Unrolling.v
 src/Util/Logic/ImplAnd.v
 src/Util/Sigma/Associativity.v
 src/Util/Sigma/Lift.v
-- 
cgit v1.2.3