diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-24 12:54:47 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-04-25 11:27:23 -0400 |
| commit | cb4f549f83d46a84c119b4c412b4c6aae64f153e (patch) | |
| tree | bbd4d32f508ea1ce7c55a83242b94156caf1fd36 /_CoqProject | |
| parent | a87912723c5b03bc5a17a9a3621abe890ee8c601 (diff) | |
Add loop invariant framework for for-loops
Also fix bugs in for-loop definition to make the proofs go through
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 3 |
1 files changed, 3 insertions, 0 deletions
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 |