Replace lists by sequences in Ortac/QCheck-STM tests

plugins/qcheck-stm/test/all_warnings.mli

@@ -1,13 +1,13 @@
 (*@ predicate p (x : 'a) = true *)
 
 type 'a t = { v : 'a array }
-(*@ mutable model contents : 'a list *)
+(*@ mutable model contents : 'a sequence *)
 
 type s
 
 val make : int -> 'a -> 'a t
 (*@ t = make i a
-    ensures t.contents = List.init i (fun _ -> a) *)
+    ensures t.contents = Sequence.init i (fun _ -> a) *)
 
 val constant : unit
 (*@ constant
@@ -47,7 +47,7 @@ val ghost_returned_value : 'a t -> bool
 
 val unsupported_quantification : 'a t -> bool
 (*@ b = unsupported_quantification t
-    ensures b = forall a. List.mem a t.contents -> p a *)
+    ensures b = forall a. Sequence.mem a t.contents -> p a *)
 
 val record_not_model_field : 'a t -> bool
 (*@ b = record_not_model_field t

plugins/qcheck-stm/test/all_warnings_errors.expected

@@ -59,14 +59,14 @@ File "all_warnings.mli", line 36, characters 0-66:
 36 | val type_not_supported : 'a t -> s
 37 | (*@ s = type_not_supported t *)
 Warning: Incomplete computation of the returned value in the specification of type_not_supported. Failure message won't be able to display the expected returned value.
-File "all_warnings.mli", line 48, characters 0-140:
+File "all_warnings.mli", line 48, characters 0-144:
 48 | val unsupported_quantification : 'a t -> bool
 49 | (*@ b = unsupported_quantification t
-50 |     ensures b = forall a. List.mem a t.contents -> p a *)
+50 |     ensures b = forall a. Sequence.mem a t.contents -> p a *)
 Warning: Incomplete computation of the returned value in the specification of unsupported_quantification. Failure message won't be able to display the expected returned value.
-File "all_warnings.mli", line 50, characters 16-54:
-50 |     ensures b = forall a. List.mem a t.contents -> p a *)
-                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+File "all_warnings.mli", line 50, characters 16-58:
+50 |     ensures b = forall a. Sequence.mem a t.contents -> p a *)
+                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Warning: Skipping clause: unsupported quantification.
 File "all_warnings.mli", line 52, characters 0-111:
 52 | val record_not_model_field : 'a t -> bool

plugins/qcheck-stm/test/conjunctive_clauses.mli

@@ -1,16 +1,13 @@
 type 'a t
-(*@ mutable model contents : 'a list *)
+(*@ mutable model contents : 'a sequence *)
 
 val make : int -> 'a -> 'a t
 (*@ t = make i a
     checks i >= 0
-    ensures true /\ true && t.contents = List.init i (fun _ -> a) *)
-
-(*@ function set_contents (c : 'a list) (i : integer) (a : 'a) : 'a list =
-          List.mapi (fun j x -> if i = j then a else x) c *)
+    ensures true /\ true && t.contents = Sequence.init i (fun _ -> a) *)
 
 val set : 'a t -> int -> 'a -> unit
 (*@ set t i a
-    checks 0 <= i < List.length t.contents
+    checks 0 <= i < Sequence.length t.contents
     modifies t
-    ensures true /\ true && t.contents = set_contents (old t.contents) i a *)
+    ensures true /\ true && t.contents = Sequence.set (old t.contents) i a *)