1 files changed, 7 insertions, 14 deletions
diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v
index 39f4a60e..a25d9c33 100644
--- a/tests/coq/misc/External_FunsExternal.v
+++ b/tests/coq/misc/External_FunsExternal.v
@@ -9,22 +9,15 @@ Require Export External_Types.
 Include External_Types.
 Module External_FunsExternal.
 
-(** [core::mem::swap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-Definition core_mem_swap (T : Type) (x : T) (y : T) (s : state) :=
-  Ok (s, (y, x))
+Axiom core_cell_Cell_get :
+  forall(T : Type) (markerCopyInst : core_marker_Copy_t T),
+        core_cell_Cell_t T -> state -> result (state * T)
 .
 
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
-Axiom core_num_nonzero_NonZeroU32_new
-  : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
-.
-
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-Axiom core_option_Option_unwrap :
-  forall(T : Type), option T -> state -> result (state * T)
+Axiom core_cell_Cell_get_mut :
+  forall(T : Type),
+        core_cell_Cell_t T -> state -> result (state * (T * (T -> state ->
+          result (state * (core_cell_Cell_t T)))))
 .
 
 End External_FunsExternal.