From 43c5265c24bd1df125f8de00d1f89379a920659a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 14 Nov 2016 21:46:40 -0500 Subject: 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. --- _CoqProject | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to '_CoqProject') 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 -- cgit v1.2.3