2 files changed, 39 insertions, 16 deletions
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 1a0014c0..e8230fad 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -42,7 +42,7 @@ Inductive Enum_t := | Enum_Variant1 : Enum_t | Enum_Variant2 : Enum_t.
 
 (** [no_nested_borrows::EmptyStruct]
     Source: 'src/no_nested_borrows.rs', lines 39:0-39:22 *)
-Record EmptyStruct_t := mkEmptyStruct_t {  }.
+Definition EmptyStruct_t : Type := unit.
 
 (** [no_nested_borrows::Sum]
     Source: 'src/no_nested_borrows.rs', lines 41:0-41:20 *)
@@ -644,4 +644,36 @@ Definition test_shared_borrow_enum1 (l : List_t u32) : result u32 :=
 Definition test_shared_borrow_enum2 : result u32 :=
   Return 0%u32.
 
+(** [no_nested_borrows::Tuple]
+    Source: 'src/no_nested_borrows.rs', lines 530:0-530:24 *)
+Definition Tuple_t (T1 T2 : Type) : Type := T1 * T2.
+
+(** [no_nested_borrows::use_tuple_struct]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/no_nested_borrows.rs', lines 532:0-532:48 *)
+Definition use_tuple_struct (x : Tuple_t u32 u32) : result (Tuple_t u32 u32) :=
+  let (_, i) := x in Return (1%u32, i)
+.
+
+(** [no_nested_borrows::create_tuple_struct]: forward function
+    Source: 'src/no_nested_borrows.rs', lines 536:0-536:61 *)
+Definition create_tuple_struct
+  (x : u32) (y : u64) : result (Tuple_t u32 u64) :=
+  Return (x, y)
+.
+
+(** [no_nested_borrows::IdType]
+    Source: 'src/no_nested_borrows.rs', lines 541:0-541:20 *)
+Definition IdType_t (T : Type) : Type := T.
+
+(** [no_nested_borrows::use_id_type]: forward function
+    Source: 'src/no_nested_borrows.rs', lines 543:0-543:40 *)
+Definition use_id_type (T : Type) (x : IdType_t T) : result T :=
+  Return x.
+
+(** [no_nested_borrows::create_id_type]: forward function
+    Source: 'src/no_nested_borrows.rs', lines 547:0-547:43 *)
+Definition create_id_type (T : Type) (x : T) : result (IdType_t T) :=
+  Return x.
+
 End NoNestedBorrows.
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 549a7116..2448e8f3 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -223,18 +223,11 @@ Definition h4
 
 (** [traits::TestType]
     Source: 'src/traits.rs', lines 122:0-122:22 *)
-Record TestType_t (T : Type) := mkTestType_t { testType_0 : T; }.
-
-Arguments mkTestType_t { _ }.
-Arguments testType_0 { _ }.
+Definition TestType_t (T : Type) : Type := T.
 
 (** [traits::{traits::TestType<T>#6}::test::TestType1]
     Source: 'src/traits.rs', lines 127:8-127:24 *)
-Record TestType_test_TestType1_t :=
-mkTestType_test_TestType1_t {
-  testType_test_TestType1_0 : u64;
-}
-.
+Definition TestType_test_TestType1_t : Type := u64.
 
 (** Trait declaration: [traits::{traits::TestType<T>#6}::test::TestTrait]
     Source: 'src/traits.rs', lines 128:8-128:23 *)
@@ -249,7 +242,7 @@ Arguments TestType_test_TestTrait_t_test { _ }.
     Source: 'src/traits.rs', lines 139:12-139:34 *)
 Definition testType_test_TestType1_test
   (self : TestType_test_TestType1_t) : result bool :=
-  Return (self.(testType_test_TestType1_0) s> 1%u64)
+  Return (self s> 1%u64)
 .
 
 (** Trait implementation: [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}]
@@ -266,14 +259,12 @@ Definition testType_test
   result bool
   :=
   x0 <- toU64TInst.(ToU64_t_to_u64) x;
-  if x0 s> 0%u64
-  then testType_test_TestType1_test {| testType_test_TestType1_0 := 0%u64 |}
-  else Return false
+  if x0 s> 0%u64 then testType_test_TestType1_test 0%u64 else Return false
 .
 
 (** [traits::BoolWrapper]
     Source: 'src/traits.rs', lines 150:0-150:22 *)
-Record BoolWrapper_t := mkBoolWrapper_t { boolWrapper_0 : bool; }.
+Definition BoolWrapper_t : Type := bool.
 
 (** [traits::{traits::BoolWrapper#7}::to_type]: forward function
     Source: 'src/traits.rs', lines 156:4-156:25 *)
@@ -281,7 +272,7 @@ Definition boolWrapper_to_type
   (T : Type) (toTypeBoolTInst : ToType_t bool T) (self : BoolWrapper_t) :
   result T
   :=
-  toTypeBoolTInst.(ToType_t_to_type) self.(boolWrapper_0)
+  toTypeBoolTInst.(ToType_t_to_type) self
 .
 
 (** Trait implementation: [traits::{traits::BoolWrapper#7}]