From 9cc912e2414870df85ffc4dd346ade5dba2b5c37 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 3 Feb 2024 00:00:36 +0100
Subject: Fix minor issues

---
 tests/fstar-split/arrays/Arrays.Clauses.fst | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'tests/fstar-split')

diff --git a/tests/fstar-split/arrays/Arrays.Clauses.fst b/tests/fstar-split/arrays/Arrays.Clauses.fst
index 68cbf216..aca328c2 100644
--- 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 =
-- 
cgit v1.2.3