snapshot

Author: cmester0

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)

examples/coverage/src/test_arrays.rs

@@ -1,4 +1,3 @@
-
 // // This function borrows a slice.
 // fn analyze_slice(slice: &[i32]) {
 //     let _ = slice[0];

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