From 744f70fc331944a12e7611a896c7dae768eebfae Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 25 Jan 2024 17:46:49 +0100 Subject: [PATCH] fix(kyber/fstar): update makefile --- proofs/fstar/extraction-edited/Makefile | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/proofs/fstar/extraction-edited/Makefile b/proofs/fstar/extraction-edited/Makefile index 54eec389..3d3cdaaa 100644 --- a/proofs/fstar/extraction-edited/Makefile +++ b/proofs/fstar/extraction-edited/Makefile @@ -80,10 +80,7 @@ VERIFIED = \ Libcrux.Kem.Kyber.Ntt.fsti \ Libcrux.Kem.Kyber.Ntt.fst \ Libcrux.Kem.Kyber.Sampling.fst \ - Libcrux.Kem.Kyber.Serialize.PartA.fsti \ - Libcrux.Kem.Kyber.Serialize.PartA.fst \ - Libcrux.Kem.Kyber.Serialize.PartB.fsti \ - Libcrux.Kem.Kyber.Serialize.PartB.fst \ + Libcrux.Kem.Kyber.Serialize.fsti \ Libcrux.Kem.Kyber.Serialize.fst UNVERIFIED =