snapshot

hacspec · Nov 26, 2024 · ddec63c · ddec63c
1 parent 3566660
commit ddec63c
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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