diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-09 15:55:37 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-09 15:55:37 -0400 |
| commit | 1eb3ce168f8ec11821c14bf856cdd0725b236cc0 (patch) | |
| tree | f7540351d76c056264b5e30d89d05a9bcd57dca2 /_CoqProject | |
| parent | b68f013b14d7725579f5b680982c2131dee93f79 (diff) | |
Some work on x86 and bounded repeated things
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index f8f0fd27d..5f348b3ee 100644 --- a/_CoqProject +++ b/_CoqProject @@ -28,6 +28,7 @@ src/BoundedArithmetic/ArchitectureToZLikeProofs.v src/BoundedArithmetic/Interface.v src/BoundedArithmetic/InterfaceProofs.v src/BoundedArithmetic/StripCF.v +src/BoundedArithmetic/X86ToZLike.v src/BoundedArithmetic/Double/Core.v src/BoundedArithmetic/Double/Proofs/BitwiseOr.v src/BoundedArithmetic/Double/Proofs/Decode.v @@ -36,6 +37,12 @@ src/BoundedArithmetic/Double/Proofs/Multiply.v src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v src/BoundedArithmetic/Double/Proofs/SelectConditional.v src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v +src/BoundedArithmetic/Double/Repeated/Core.v +src/BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr.v +src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v +src/BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate.v +src/BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub.v +src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v |