2 files changed, 35 insertions, 6 deletions
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 130b02f2..0c66d3ac 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -560,3 +560,32 @@ let test_shared_borrow_enum1 (l : list_t u32) : result u32 =
 let test_shared_borrow_enum2 : result u32 =
   Return 0
 
+(** [no_nested_borrows::Tuple]
+    Source: 'src/no_nested_borrows.rs', lines 530:0-530:24 *)
+type tuple_t (t1 t2 : Type0) = 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 *)
+let use_tuple_struct (x : tuple_t u32 u32) : result (tuple_t u32 u32) =
+  let (_, i) = x in Return (1, i)
+
+(** [no_nested_borrows::create_tuple_struct]: forward function
+    Source: 'src/no_nested_borrows.rs', lines 536:0-536:61 *)
+let 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 *)
+type idType_t (t : Type0) = t
+
+(** [no_nested_borrows::use_id_type]: forward function
+    Source: 'src/no_nested_borrows.rs', lines 543:0-543:40 *)
+let use_id_type (t : Type0) (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 *)
+let create_id_type (t : Type0) (x : t) : result (idType_t t) =
+  Return x
+
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 8252aad4..7d504cb5 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -177,11 +177,11 @@ let h4
 
 (** [traits::TestType]
     Source: 'src/traits.rs', lines 122:0-122:22 *)
-type testType_t (t : Type0) = { _0 : t; }
+type testType_t (t : Type0) = t
 
 (** [traits::{traits::TestType<T>#6}::test::TestType1]
     Source: 'src/traits.rs', lines 127:8-127:24 *)
-type testType_test_TestType1_t = { _0 : u64; }
+type testType_test_TestType1_t = u64
 
 (** Trait declaration: [traits::{traits::TestType<T>#6}::test::TestTrait]
     Source: 'src/traits.rs', lines 128:8-128:23 *)
@@ -193,7 +193,7 @@ noeq type testType_test_TestTrait_t (self : Type0) = {
     Source: 'src/traits.rs', lines 139:12-139:34 *)
 let testType_test_TestType1_test
   (self : testType_test_TestType1_t) : result bool =
-  Return (self._0 > 1)
+  Return (self > 1)
 
 (** Trait implementation: [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}]
     Source: 'src/traits.rs', lines 138:8-138:36 *)
@@ -209,11 +209,11 @@ let testType_test
   result bool
   =
   let* x0 = toU64TInst.to_u64 x in
-  if x0 > 0 then testType_test_TestType1_test { _0 = 0 } else Return false
+  if x0 > 0 then testType_test_TestType1_test 0 else Return false
 
 (** [traits::BoolWrapper]
     Source: 'src/traits.rs', lines 150:0-150:22 *)
-type boolWrapper_t = { _0 : bool; }
+type boolWrapper_t = bool
 
 (** [traits::{traits::BoolWrapper#7}::to_type]: forward function
     Source: 'src/traits.rs', lines 156:4-156:25 *)
@@ -221,7 +221,7 @@ let boolWrapper_to_type
   (t : Type0) (toTypeBoolTInst : toType_t bool t) (self : boolWrapper_t) :
   result t
   =
-  toTypeBoolTInst.to_type self._0
+  toTypeBoolTInst.to_type self
 
 (** Trait implementation: [traits::{traits::BoolWrapper#7}]
     Source: 'src/traits.rs', lines 152:0-152:33 *)