#define Hacl_Curve25519_64_Local_scalarmult Hacl_Curve25519_64_scalarmult
#define Hacl_Curve25519_64_Local_secret_to_public Hacl_Curve25519_64_secret_to_public
#define Hacl_Curve25519_64_Local_ecdh Hacl_Curve25519_64_ecdh