diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-10 14:55:34 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-10 14:55:34 -0400 |
| commit | a75c0c7dd83e2b1b92784b4d5d7a222f6fe9bc52 (patch) | |
| tree | 4087e14e05c9a59ab29811a4c9c730c7a83971c0 /_CoqProject | |
| parent | fa38b037a4b9e26a7153938c2c650966297d0d67 (diff) | |
Add some admitted x86->ZLike proofs
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index f672639ee..f8420855e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -29,6 +29,7 @@ src/BoundedArithmetic/Interface.v src/BoundedArithmetic/InterfaceProofs.v src/BoundedArithmetic/StripCF.v src/BoundedArithmetic/X86ToZLike.v +src/BoundedArithmetic/X86ToZLikeProofs.v src/BoundedArithmetic/Double/Core.v src/BoundedArithmetic/Double/Proofs/BitwiseOr.v src/BoundedArithmetic/Double/Proofs/Decode.v |