renamed theorem to accurately reflect property

verse-lab · Oct 4, 2019 · ce81d6d · ce81d6d
1 parent 3879ef3
commit ce81d6d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Structures/BloomFilter/Probability.v b/Structures/BloomFilter/Probability.v
@@ -1559,7 +1559,7 @@ Section BloomFilter.
       }
   Qed.
 
-  Theorem bloomfilter_no_false_positives l  bf (hashes: hash_vec) x xs :
+  Theorem bloomfilter_no_false_negatives l  bf (hashes: hash_vec) x xs :
     uniq (x :: xs) ->
     length xs == l ->
     hashes_have_free_spaces hashes (l.+1) ->