Regenerate the Coq test files

3 files changed, 16 insertions, 37 deletions

diff --git a/tests/coq/array/Array_Funs.v b/tests/coq/array/Array.v
index 9980a6e8..825f73e0 100644
--- a/tests/coq/array/Array_Funs.v
+++ b/tests/coq/array/Array.v
@@ -1,14 +1,15 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [array]: function definitions *)
+(** [array] *)
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export Array_Types.
-Import Array_Types.
-Module Array_Funs.
+Module Array.
+
+(** [array::AB] *)
+Inductive AB_t := | AB_A : AB_t | AB_B : AB_t.
 
 (** [array::incr]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
@@ -98,7 +99,7 @@ Definition index_mut_slice_back
 
 (** [array::slice_subslice_shared_]: forward function *)
 Definition slice_subslice_shared_
-  (n : nat) (x : slice u32) (y : usize) (z : usize) : result (slice u32) :=
+  (x : slice u32) (y : usize) (z : usize) : result (slice u32) :=
   core_slice_index_Slice_index u32 (core_ops_range_Range usize)
     (core_slice_index_Range_coresliceindexSliceIndexInst u32) x
     {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |}
@@ -106,7 +107,7 @@ Definition slice_subslice_shared_
 
 (** [array::slice_subslice_mut_]: forward function *)
 Definition slice_subslice_mut_
-  (n : nat) (x : slice u32) (y : usize) (z : usize) : result (slice u32) :=
+  (x : slice u32) (y : usize) (z : usize) : result (slice u32) :=
   core_slice_index_Slice_index_mut u32 (core_ops_range_Range usize)
     (core_slice_index_Range_coresliceindexSliceIndexInst u32) x
     {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |}
@@ -114,7 +115,7 @@ Definition slice_subslice_mut_
 
 (** [array::slice_subslice_mut_]: backward function 0 *)
 Definition slice_subslice_mut__back
-  (n : nat) (x : slice u32) (y : usize) (z : usize) (ret : slice u32) :
+  (x : slice u32) (y : usize) (z : usize) (ret : slice u32) :
   result (slice u32)
   :=
   core_slice_index_Slice_index_mut_back u32 (core_ops_range_Range usize)
@@ -141,9 +142,7 @@ Definition array_to_slice_mut__back
 
 (** [array::array_subslice_shared_]: forward function *)
 Definition array_subslice_shared_
-  (n : nat) (x : array u32 32%usize) (y : usize) (z : usize) :
-  result (slice u32)
-  :=
+  (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) :=
   core_array_Array_index u32 (core_ops_range_Range usize) 32%usize
     (core_slice_index_Slice_coreopsindexIndexInst u32 (core_ops_range_Range
     usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x
@@ -152,9 +151,7 @@ Definition array_subslice_shared_
 
 (** [array::array_subslice_mut_]: forward function *)
 Definition array_subslice_mut_
-  (n : nat) (x : array u32 32%usize) (y : usize) (z : usize) :
-  result (slice u32)
-  :=
+  (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) :=
   core_array_Array_index_mut u32 (core_ops_range_Range usize) 32%usize
     (core_slice_index_Slice_coreopsindexIndexMutInst u32 (core_ops_range_Range
     usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x
@@ -163,8 +160,7 @@ Definition array_subslice_mut_
 
 (** [array::array_subslice_mut_]: backward function 0 *)
 Definition array_subslice_mut__back
-  (n : nat) (x : array u32 32%usize) (y : usize) (z : usize) (ret : slice u32)
-  :
+  (x : array u32 32%usize) (y : usize) (z : usize) (ret : slice u32) :
   result (array u32 32%usize)
   :=
   core_array_Array_index_mut_back u32 (core_ops_range_Range usize) 32%usize
@@ -310,7 +306,7 @@ Definition update_all : result unit :=
 .
 
 (** [array::range_all]: forward function *)
-Definition range_all (n : nat) : result unit :=
+Definition range_all : result unit :=
   s <-
     core_array_Array_index_mut u32 (core_ops_range_Range usize) 4%usize
       (core_slice_index_Slice_coreopsindexIndexMutInst u32
@@ -432,9 +428,7 @@ Definition f2 (i : u32) : result unit :=
 
 (** [array::f4]: forward function *)
 Definition f4
-  (n : nat) (x : array u32 32%usize) (y : usize) (z : usize) :
-  result (slice u32)
-  :=
+  (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) :=
   core_array_Array_index u32 (core_ops_range_Range usize) 32%usize
     (core_slice_index_Slice_coreopsindexIndexInst u32 (core_ops_range_Range
     usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x
@@ -449,7 +443,7 @@ Definition f3 (n : nat) : result u32 :=
   _ <- f2 i;
   let b := array_repeat u32 32%usize 0%u32 in
   s <- array_to_slice u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]);
-  s0 <- f4 n b 16%usize 18%usize;
+  s0 <- f4 b 16%usize 18%usize;
   sum2 n s s0
 .
 
@@ -473,4 +467,4 @@ Definition ite : result unit :=
   Return tt
 .
 
-End Array_Funs .
+End Array .
diff --git a/tests/coq/array/Array_Types.v b/tests/coq/array/Array_Types.v
deleted file mode 100644
index a13d64e6..00000000
--- a/tests/coq/array/Array_Types.v
+++ /dev/null
@@ -1,14 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [array]: type definitions *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Require Import List.
-Import ListNotations.
-Local Open Scope Primitives_scope.
-Module Array_Types.
-
-(** [array::AB] *)
-Inductive AB_t := | AB_A : AB_t | AB_B : AB_t.
-
-End Array_Types .
diff --git a/tests/coq/array/_CoqProject b/tests/coq/array/_CoqProject
index f33cefe6..87d8fc3d 100644
--- a/tests/coq/array/_CoqProject
+++ b/tests/coq/array/_CoqProject
@@ -3,6 +3,5 @@
 -arg -w
 -arg all
 
-Array_Funs.v
 Primitives.v
-Array_Types.v
+Array.v