From 08be7fa27881cf4bef5bede9d07feaaa9025b9a4 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 28 Apr 2017 20:28:08 -0400 Subject: Prove relationship between `xzladderstep` and M.add (#162) * hopefully all proofs we need about xzladderstep * Better automation in xzproofs * Speed up xzproofs with heuristic clearing * Remove useless hypotheses * XZProofs cleanup * fix "group by isomorphism" proofs, use in XZProofs --- _CoqProject | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index 1e3cc61ec..7b3b2358b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -142,10 +142,10 @@ src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v src/Compilers/Z/Syntax/Equality.v src/Compilers/Z/Syntax/Util.v src/Curves/Edwards/AffineProofs.v -src/Curves/Edwards/Montgomery.v src/Curves/Edwards/Pre.v src/Curves/Edwards/XYZT.v src/Curves/Montgomery/Affine.v +src/Curves/Montgomery/AffineInstances.v src/Curves/Montgomery/AffineProofs.v src/Curves/Montgomery/XZ.v src/Curves/Montgomery/XZProofs.v -- cgit v1.2.3