diff options
Diffstat (limited to 'tests/src/hashmap.rs')
| -rw-r--r-- | tests/src/hashmap.rs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs index 9ff448db..12a95d0f 100644 --- a/tests/src/hashmap.rs +++ b/tests/src/hashmap.rs @@ -1,7 +1,7 @@ //@ charon-args=--opaque=utils //@ [!borrow-check] aeneas-args=-state -split-files //@ [coq] aeneas-args=-use-fuel -//@ [fstar] aeneas-args=-decreases-clauses -template-clauses +//@ [fstar] aeneas-args=-decreases-clauses //@ [lean] aeneas-args=-no-gen-lib-entry // ^ the `-no-gen-lib-entry` is because we add a custom import in the Hashmap.lean file: we do not // want to overwrite it. |