aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Assembly/GF25519.v3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v
index 3f3c34b71..e1ecfdce0 100644
--- a/src/Assembly/GF25519.v
+++ b/src/Assembly/GF25519.v
@@ -303,8 +303,9 @@ Module GF25519.
Definition opp := Eval simpl in proj1_sig opp'.
End Instantiation.
End GF25519.
-
+(*
Extraction "GF25519Add" GF25519.Add.
Extraction "GF25519Sub" GF25519.Sub.
Extraction "GF25519Mul" GF25519.Mul.
Extraction "GF25519Opp" GF25519.Opp.
+*)