diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/src/loops.rs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tests/src/loops.rs b/tests/src/loops.rs index 2f71d75b..afc52ace 100644 --- a/tests/src/loops.rs +++ b/tests/src/loops.rs @@ -1,3 +1,7 @@ +//@ [coq] aeneas-args=-use-fuel +//@ [fstar] aeneas-args=-decreases-clauses -template-clauses +//@ [fstar] aeneas-args=-split-files +//@ [coq,fstar] subdir=misc use std::vec::Vec; /// No borrows |