diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml
index ba8134a56..fddc6757b 100644
--- a/engine/backends/coq/coq/coq_backend.ml
+++ b/engine/backends/coq/coq/coq_backend.ml
@@ -623,7 +623,7 @@ struct
              ^^ break 1))
         ^^ break 1
         ^^ CoqNotation.arguments (!^"Build_" ^^ name#p)
-          arguments_explicity_without_ty (* arguments_explicity_with_ty *)
+             arguments_explicity_without_ty (* arguments_explicity_with_ty *)
         ^^ concat_map_with ~pre:(break 1)
              (fun (ident, typ, attr) ->
                CoqNotation.arguments ident#p arguments_explicity_without_ty)
diff --git a/examples/coverage/src/test_arrays.rs b/examples/coverage/src/test_arrays.rs
index d6ab14e11..939f85f73 100644
--- a/examples/coverage/src/test_arrays.rs
+++ b/examples/coverage/src/test_arrays.rs
@@ -1,4 +1,3 @@
-
 // // This function borrows a slice.
 // fn analyze_slice(slice: &[i32]) {
 //     let _ = slice[0];
diff --git a/test-harness/src/snapshots/toolchain__slices into-coq.snap b/test-harness/src/snapshots/toolchain__slices into-coq.snap
index e3c7b6e84..80cde0df4 100644
--- a/test-harness/src/snapshots/toolchain__slices into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__slices into-coq.snap	
@@ -55,7 +55,7 @@ Definition r#unsized '(_ : t_Array (t_Slice t_u8) ((1 : t_usize))) : unit :=
   tt.
 
 Definition sized (x : t_Array (t_Array (t_u8) ((4 : t_usize))) ((1 : t_usize))) : unit :=
-  r#unsized ([unsize (index (x) ((0 : t_usize)))]).
+  r#unsized ([unsize (Index_f_index (x) ((0 : t_usize)))]).
 '''
 _CoqProject = '''
 -R ./ TODO