pending

formosa-crypto · Nov 27, 2024 · 6b9af15 · 6b9af15
1 parent 3491684
commit 6b9af15
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 3 deletions.
diff --git a/easycrypt.project b/easycrypt.project
@@ -6,11 +6,9 @@ provers = [email protected]
 provers = [email protected]
 
 rdirs = proof
-rdirs = ../easycrypt/examples
 rdirs = Jasmin:jasmin/eclib
 idirs = code/jasmin/mlkem_ref/extraction
 idirs = code/jasmin/mlkem_avx2/extraction
 idirs = crypto-specs/common
 rdirs = crypto-specs/fips202
 rdirs = crypto-specs/ml-kem
-rdirs = ~/Desktop/Repos/easycrypt/examples
diff --git a/proof/security/MLWE_PKE.ec b/proof/security/MLWE_PKE.ec
@@ -1,4 +1,4 @@
-require import AllCore Distr List SmtMap Dexcepted PKE_ROM.
+require import AllCore Distr List FMap Dexcepted PKE_ROM.
 require (****) RndExcept StdOrder MLWE.
 
 theory MLWE_PKE.