From 761259c947ebe2ba94c71b5121b6790bc6d9d1e6 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 28 Feb 2016 16:33:06 -0500 Subject: ModularArithmetic: [field] tactic that respects opacity, prettify ExtendedCoordinates, outline Edwards curve associativity --- _CoqProject | 1 + 1 file changed, 1 insertion(+) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index c1a88976f..3adab537f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -7,6 +7,7 @@ src/CompleteEdwardsCurve/DoubleAndAdd.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v src/Encoding/EncodingTheorems.v +src/ModularArithmetic/FField.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v src/ModularArithmetic/Pre.v -- cgit v1.2.3