diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-14 21:46:40 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-14 21:46:40 -0500 |
| commit | 43c5265c24bd1df125f8de00d1f89379a920659a (patch) | |
| tree | fdb435c27c7fa1fdc22c9ca8cf107e52dc094a5c /_CoqProject | |
| parent | 4faedd36b571f6c07eab1e348d1df655e1123eda (diff) | |
Support for 128-bit words
I haven't found a good way to genericize the proofs of relatedness
things, mostly because Modules and functors are annoying.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/_CoqProject b/_CoqProject index 4a1246cf7..082d9d0d3 100644 --- a/_CoqProject +++ b/_CoqProject @@ -125,12 +125,15 @@ src/Reflection/Named/EstablishLiveness.v src/Reflection/Named/NameUtil.v src/Reflection/Named/RegisterAssign.v src/Reflection/Named/Syntax.v -src/Reflection/Z/Interpretations.v +src/Reflection/Z/Interpretations128.v +src/Reflection/Z/Interpretations64.v src/Reflection/Z/InterpretationsGen.v src/Reflection/Z/Reify.v src/Reflection/Z/Syntax.v -src/Reflection/Z/Interpretations/Relations.v -src/Reflection/Z/Interpretations/RelationsCombinations.v +src/Reflection/Z/Interpretations128/Relations.v +src/Reflection/Z/Interpretations128/RelationsCombinations.v +src/Reflection/Z/Interpretations64/Relations.v +src/Reflection/Z/Interpretations64/RelationsCombinations.v src/Spec/CompleteEdwardsCurve.v src/Spec/Ed25519.v src/Spec/EdDSA.v |