Fix minor issues

AeneasVerif · Feb 2, 2024 · 9cc912e · 9cc912e
1 parent 3157013
commit 9cc912e
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 10 deletions.
diff --git a/tests/fstar-split/arrays/Arrays.Clauses.fst b/tests/fstar-split/arrays/Arrays.Clauses.fst
@@ -1,17 +1,17 @@
-(** [array]: decreases clauses *)
-module Array.Clauses
+(** [arrays]: decreases clauses *)
+module Arrays.Clauses
 open Primitives
-open Array.Types
+open Arrays.Types
 open FStar.List.Tot
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [array::sum]: decreases clause *)
+(** [arrays::sum]: decreases clause *)
 unfold
 let sum_loop_decreases (s : slice u32) (sum : u32) (i : usize) : nat =
   if i < length s then length s - i else 0
 
-(** [array::sum2]: decreases clause *)
+(** [arrays::sum2]: decreases clause *)
 unfold
 let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum : u32)
   (i : usize) : nat =

diff --git a/tests/fstar/arrays/Arrays.Clauses.fst b/tests/fstar/arrays/Arrays.Clauses.fst
@@ -1,17 +1,17 @@
-(** [array]: decreases clauses *)
-module Array.Clauses
+(** [arrays]: decreases clauses *)
+module Arrays.Clauses
 open Primitives
-open Array.Types
+open Arrays.Types
 open FStar.List.Tot
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [array::sum]: decreases clause *)
+(** [arrays::sum]: decreases clause *)
 unfold
 let sum_loop_decreases (s : slice u32) (sum : u32) (i : usize) : nat =
   if i < length s then length s - i else 0
 
-(** [array::sum2]: decreases clause *)
+(** [arrays::sum2]: decreases clause *)
 unfold
 let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum : u32)
   (i : usize) : nat =