From b0ff2c5564db3c3edfbd9db2015c7e0e17649da5 Mon Sep 17 00:00:00 2001 From: mamonet Date: Wed, 11 Dec 2024 07:54:56 +0000 Subject: [PATCH] Put Vector.Rej_sample_table in SLOW_MODULES --- libcrux-ml-kem/proofs/fstar/extraction/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 \