aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-08-23 15:59:35 -0700
committerGravatar Jason Gross <jagro@google.com>2016-08-23 16:01:54 -0700
commit6897a4f42c86c4a6bfdbab6887276e7334317661 (patch)
treef5f283d445622171d09584af9ca0ac652c589d3a /_CoqProject
parente7554f5525a36699fff33e70ee454cfd0a687808 (diff)
Hook up the bounded interface, finish proofs
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject1
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index 5c08e1616..caee0caff 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -24,6 +24,7 @@ src/Assembly/Vectorize.v
src/Assembly/Wordize.v
src/BoundedArithmetic/ArchitectureToZLike.v
src/BoundedArithmetic/DoubleBounded.v
+src/BoundedArithmetic/DoubleBoundedProofs.v
src/BoundedArithmetic/Interface.v
src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
src/CompleteEdwardsCurve/ExtendedCoordinates.v