diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Makefile b/libcrux-ml-kem/proofs/fstar/extraction/Makefile index 4b9b03c26..7865c6d43 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Makefile +++ b/libcrux-ml-kem/proofs/fstar/extraction/Makefile @@ -1,7 +1,7 @@ -SLOW_MODULES += Libcrux_ml_kem.Vector.Portable.Serialize.fst +SLOW_MODULES += Libcrux_ml_kem.Vector.Portable.Serialize.fst \ + Libcrux_ml_kem.Vector.Rej_sample_table.fsti -ADMIT_MODULES = Libcrux_ml_kem.Vector.Rej_sample_table.fsti \ - Libcrux_ml_kem.Vector.Neon.Arithmetic.fst \ +ADMIT_MODULES = Libcrux_ml_kem.Vector.Neon.Arithmetic.fst \ Libcrux_ml_kem.Vector.Neon.Compress.fst \ Libcrux_ml_kem.Vector.Neon.fsti \ Libcrux_ml_kem.Vector.Neon.fst \