aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar jadep <jade.philipoom@gmail.com>2016-04-19 21:00:42 -0400
committerGravatar jadep <jade.philipoom@gmail.com>2016-04-19 21:00:42 -0400
commit9e0f6e02dcf1c2884a41cfd539cc371bbbf6ae76 (patch)
treebe9a9a24de167661915cd714d23cc7832f977a31 /_CoqProject
parent7afde2d5e17ffa15915ea6b49c0705883636199a (diff)
Defined a testbit variant for BaseSystem vectors and proved equivalence to Z.testbit.
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject1
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index 04b25dd6c..9e1717dd5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -28,6 +28,7 @@ src/Spec/PointEncoding.v
src/Specific/Ed25519.v
src/Specific/GF25519.v
src/Tactics/VerdiTactics.v
+src/Testbit.v
src/Util/CaseUtil.v
src/Util/IterAssocOp.v
src/Util/ListUtil.v