diff options
Diffstat (limited to 'tests/src/loops.rs')
-rw-r--r-- | tests/src/loops.rs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tests/src/loops.rs b/tests/src/loops.rs index 8692c60e..afc52ace 100644 --- a/tests/src/loops.rs +++ b/tests/src/loops.rs @@ -1,6 +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 |