aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/X2555/C128/Synthesis.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-11-12 18:13:00 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-11-12 18:13:00 -0500
commitaeedfe5bd2f49ce1a3e9905d2c7291472044e8ad (patch)
tree1addbcb1ed6afd25d5ad109be443672dd8e11a5d /src/Specific/X2555/C128/Synthesis.v
parent9f7c3c49118b907b713de3525ede966d4bd5d048 (diff)
Remove outdated C128 files
Diffstat (limited to 'src/Specific/X2555/C128/Synthesis.v')
-rw-r--r--src/Specific/X2555/C128/Synthesis.v9
1 files changed, 0 insertions, 9 deletions
diff --git a/src/Specific/X2555/C128/Synthesis.v b/src/Specific/X2555/C128/Synthesis.v
deleted file mode 100644
index af7b8ae33..000000000
--- a/src/Specific/X2555/C128/Synthesis.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Import Crypto.Specific.Framework.SynthesisFramework.
-Require Import Crypto.Specific.X2555.C128.CurveParameters.
-
-Module P <: PrePackage.
- Definition package : Tag.Context.
- Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined.
-End P.
-
-Module Export S := PackageSynthesis P.