From 7af9bcb13b75f07bb0cb14240fbeaf7931d1c736 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Thu, 7 Dec 2023 14:34:09 +0100 Subject: [PATCH] Cleanup --- proof-libs/coq/coq/_CoqProject | 20 -------------------- 1 file changed, 20 deletions(-) diff --git a/proof-libs/coq/coq/_CoqProject b/proof-libs/coq/coq/_CoqProject index 9b71d810b..923a70ebc 100644 --- a/proof-libs/coq/coq/_CoqProject +++ b/proof-libs/coq/coq/_CoqProject @@ -1,27 +1,7 @@ -R src/ Hacspec -# -Q src/_vc "" # Folder should be ignored! -arg -w -arg all src/MachineIntegers.v src/Hacspec_Lib.v src/QuickChickLib.v - -# # src/Hacspec_Coverage_Test.v -# # src/Hacspec_Aes.v # TODO: not currently working ? -# # src/Hacspec_Aes128_Gcm.v # requires Aes -# src/Hacspec_Bls12_381.v -# # src/Hacspec_Bls12_381_Hash.v -# src/Hacspec_Chacha20.v -# src/Hacspec_Poly1305.v -# # src/Hacspec_Chacha20poly1305.v -# src/Hacspec_Curve25519.v -# # src/Hacspec_Ecdsa_P256_Sha256.v -# src/Hacspec_Gf128.v -# # src/Hacspec_Gimli.v # ArrayName::length() impl missing -# # src/Hacspec_Hkdf.v # Cannot infer M for bind (should use result_monad) -# # src/Hacspec_Hmac.v -# # src/Hacspec_Ntru_Prime.v # missing mul_poly_irr /// Polynomial multiplication of two size fixed polynomials in R_modulo \ irr -# # src/Hacspec_P256.v -# # src/Hacspec_Sha3.v # Issues with operations with different types eg ".*" vs "*" -# src/Hacspec_Sha256.v