7 files changed, 134 insertions, 85 deletions

diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 41d4a7bd..c4f70f75 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -12,64 +12,33 @@ Require Import External_FunsExternal.
 Include External_FunsExternal.
 Module External_Funs.
 
-(** [external::swap]:
-    Source: 'src/external.rs', lines 6:0-6:46 *)
-Definition swap
-  (T : Type) (x : T) (y : T) (st : state) : result (state * (T * T)) :=
-  core_mem_swap T x y st
+(** Trait implementation: [core::marker::{(core::marker::Copy for u32)#40}]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 47:29-47:65
+    Name pattern: core::marker::Copy<u32> *)
+Definition core_marker_CopyU32 : core_marker_Copy_t u32 := {|
+  core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst := core_clone_CloneU32;
+|}.
+
+(** [external::use_get]:
+    Source: 'src/external.rs', lines 5:0-5:37 *)
+Definition use_get
+  (rc : core_cell_Cell_t u32) (st : state) : result (state * u32) :=
+  core_cell_Cell_get u32 core_marker_CopyU32 rc st
 .
 
-(** [external::test_new_non_zero_u32]:
-    Source: 'src/external.rs', lines 11:0-11:60 *)
-Definition test_new_non_zero_u32
-  (x : u32) (st : state) : result (state * core_num_nonzero_NonZeroU32_t) :=
-  p <- core_num_nonzero_NonZeroU32_new x st;
-  let (st1, o) := p in
-  core_option_Option_unwrap core_num_nonzero_NonZeroU32_t o st1
-.
-
-(** [external::test_vec]:
-    Source: 'src/external.rs', lines 17:0-17:17 *)
-Definition test_vec : result unit :=
-  _ <- alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0%u32; Ok tt
-.
-
-(** Unit test for [external::test_vec] *)
-Check (test_vec )%return.
-
-(** [external::custom_swap]:
-    Source: 'src/external.rs', lines 24:0-24:66 *)
-Definition custom_swap
-  (T : Type) (x : T) (y : T) (st : state) :
-  result (state * (T * (T -> state -> result (state * (T * T)))))
+(** [external::incr]:
+    Source: 'src/external.rs', lines 9:0-9:31 *)
+Definition incr
+  (rc : core_cell_Cell_t u32) (st : state) :
+  result (state * (core_cell_Cell_t u32))
   :=
-  p <- core_mem_swap T x y st;
-  let (st1, p1) := p in
-  let (x1, y1) := p1 in
-  let back := fun (ret : T) (st2 : state) => Ok (st2, (ret, y1)) in
-  Ok (st1, (x1, back))
-.
-
-(** [external::test_custom_swap]:
-    Source: 'src/external.rs', lines 29:0-29:59 *)
-Definition test_custom_swap
-  (x : u32) (y : u32) (st : state) : result (state * (u32 * u32)) :=
-  p <- custom_swap u32 x y st;
-  let (st1, p1) := p in
-  let (_, custom_swap_back) := p1 in
-  p2 <- custom_swap_back 1%u32 st1;
-  let (_, p3) := p2 in
-  let (x1, y1) := p3 in
-  Ok (st1, (x1, y1))
-.
-
-(** [external::test_swap_non_zero]:
-    Source: 'src/external.rs', lines 35:0-35:44 *)
-Definition test_swap_non_zero (x : u32) (st : state) : result (state * u32) :=
-  p <- swap u32 x 0%u32 st;
+  p <- core_cell_Cell_get_mut u32 rc st;
   let (st1, p1) := p in
-  let (x1, _) := p1 in
-  if x1 s= 0%u32 then Fail_ Failure else Ok (st1, x1)
+  let (i, get_mut_back) := p1 in
+  i1 <- u32_add i 1%u32;
+  p2 <- get_mut_back i1 st1;
+  let (_, rc1) := p2 in
+  Ok (st1, rc1)
 .
 
 End External_Funs.
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.
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 8658236f..b3e4a129 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -11,18 +11,21 @@ Require Import External_Types.
 Include External_Types.
 Module External_FunsExternal_Template.
 
-(** [core::mem::swap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
-    Name pattern: core::mem::swap *)
-Axiom core_mem_swap :
-  forall(T : Type), T -> T -> state -> result (state * (T * T))
+(** [core::cell::{core::cell::Cell<T>#10}::get]:
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 497:4-497:26
+    Name pattern: core::cell::{core::cell::Cell<@T>}::get *)
+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]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
-    Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *)
-Axiom core_num_nonzero_NonZeroU32_new
-  : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
+(** [core::cell::{core::cell::Cell<T>#11}::get_mut]:
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 574:4-574:39
+    Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *)
+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_Template.
diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v
index b42c2ecf..5b233c62 100644
--- a/tests/coq/misc/External_Types.v
+++ b/tests/coq/misc/External_Types.v
@@ -10,4 +10,14 @@ Require Import External_TypesExternal.
 Include External_TypesExternal.
 Module External_Types.
 
+(** Trait declaration: [core::marker::Copy]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 450:0-450:21
+    Name pattern: core::marker::Copy *)
+Record core_marker_Copy_t (Self : Type) := mkcore_marker_Copy_t {
+  core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst : core_clone_Clone Self;
+}.
+
+Arguments mkcore_marker_Copy_t { _ }.
+Arguments core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst { _ }.
+
 End External_Types.
diff --git a/tests/coq/misc/External_TypesExternal.v b/tests/coq/misc/External_TypesExternal.v
index 734c66e5..6bb2b1db 100644
--- a/tests/coq/misc/External_TypesExternal.v
+++ b/tests/coq/misc/External_TypesExternal.v
@@ -8,9 +8,8 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Module External_TypesExternal.
 
-(** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
-Axiom core_num_nonzero_NonZeroU32_t : Type.
+(** [core::cell::Cell] *)
+Axiom core_cell_Cell_t : forall (T : Type), Type.
 
 (** The state type used in the state-error monad *)
 Axiom state : Type.
diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v
index 7d6af202..87b1c826 100644
--- a/tests/coq/misc/External_TypesExternal_Template.v
+++ b/tests/coq/misc/External_TypesExternal_Template.v
@@ -9,10 +9,10 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Module External_TypesExternal_Template.
 
-(** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
-    Name pattern: core::num::nonzero::NonZeroU32 *)
-Axiom core_num_nonzero_NonZeroU32_t : Type.
+(** [core::cell::Cell]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 293:0-293:26
+    Name pattern: core::cell::Cell *)
+Axiom core_cell_Cell_t : forall (T : Type), Type.
 
 (** The state type used in the state-error monad *)
 Axiom state : Type.
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index e84d65ce..5ffda12f 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -489,6 +489,81 @@ Definition core_i64_max   := i64_max %i64.
 Definition core_i128_max  := i64_max %i128.
 Axiom core_isize_max : isize. (** TODO *)
 
+(*** core *)
+
+(** Trait declaration: [core::clone::Clone] *)
+Record core_clone_Clone (self : Type) := {
+  clone : self -> result self
+}.
+
+Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b.
+
+Definition core_clone_CloneBool : core_clone_Clone bool := {|
+  clone := fun b => Ok (core_clone_impls_CloneBool_clone b)
+|}.
+
+Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x.
+Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x.
+Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x.
+Definition core_clone_impls_CloneU32_clone (x : u32) : u32 := x.
+Definition core_clone_impls_CloneU64_clone (x : u64) : u64 := x.
+Definition core_clone_impls_CloneU128_clone (x : u128) : u128 := x.
+
+Definition core_clone_impls_CloneIsize_clone (x : isize) : isize := x.
+Definition core_clone_impls_CloneI8_clone (x : i8) : i8 := x.
+Definition core_clone_impls_CloneI16_clone (x : i16) : i16 := x.
+Definition core_clone_impls_CloneI32_clone (x : i32) : i32 := x.
+Definition core_clone_impls_CloneI64_clone (x : i64) : i64 := x.
+Definition core_clone_impls_CloneI128_clone (x : i128) : i128 := x.
+
+Definition core_clone_CloneUsize : core_clone_Clone usize := {|
+  clone := fun x => Ok (core_clone_impls_CloneUsize_clone x)
+|}.
+
+Definition core_clone_CloneU8 : core_clone_Clone u8 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU8_clone x)
+|}.
+
+Definition core_clone_CloneU16 : core_clone_Clone u16 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU16_clone x)
+|}.
+
+Definition core_clone_CloneU32 : core_clone_Clone u32 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU32_clone x)
+|}.
+
+Definition core_clone_CloneU64 : core_clone_Clone u64 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU64_clone x)
+|}.
+
+Definition core_clone_CloneU128 : core_clone_Clone u128 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU128_clone x)
+|}.
+
+Definition core_clone_CloneIsize : core_clone_Clone isize := {|
+  clone := fun x => Ok (core_clone_impls_CloneIsize_clone x)
+|}.
+
+Definition core_clone_CloneI8 : core_clone_Clone i8 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI8_clone x)
+|}.
+
+Definition core_clone_CloneI16 : core_clone_Clone i16 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI16_clone x)
+|}.
+
+Definition core_clone_CloneI32 : core_clone_Clone i32 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI32_clone x)
+|}.
+
+Definition core_clone_CloneI64 : core_clone_Clone i64 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI64_clone x)
+|}.
+
+Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
+|}.
+
 (*** core::ops *)
 
 (* Trait declaration: [core::ops::index::Index] *)