Regenerate the files

3 files changed, 71 insertions, 61 deletions

diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index f0875a29..93ff9fe3 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -200,12 +200,12 @@ Definition h3
 (** Trait declaration: [traits::OfTypeBis]
     Source: 'src/traits.rs', lines 109:0-109:36 *)
 Record OfTypeBis_t (Self T : Type) := mkOfTypeBis_t {
-  OfTypeBis_tOfTypeBis_t_parent_clause_0 : ToType_t T Self;
+  OfTypeBis_tOfTypeBis_t_ToTypeTSelfInst : ToType_t T Self;
   OfTypeBis_t_of_type : T -> result Self;
 }.
 
 Arguments mkOfTypeBis_t { _ _ }.
-Arguments OfTypeBis_tOfTypeBis_t_parent_clause_0 { _ _ }.
+Arguments OfTypeBis_tOfTypeBis_t_ToTypeTSelfInst { _ _ }.
 Arguments OfTypeBis_t_of_type { _ _ }.
 
 (** [traits::h4]: forward function
@@ -395,19 +395,20 @@ Arguments mkParentTrait1_t { _ }.
 (** Trait declaration: [traits::ChildTrait]
     Source: 'src/traits.rs', lines 206:0-206:49 *)
 Record ChildTrait_t (Self : Type) := mkChildTrait_t {
-  ChildTrait_tChildTrait_t_parent_clause_0 : ParentTrait0_t Self;
-  ChildTrait_tChildTrait_t_parent_clause_1 : ParentTrait1_t Self;
+  ChildTrait_tChildTrait_t_ParentTrait0SelfInst : ParentTrait0_t Self;
+  ChildTrait_tChildTrait_t_ParentTrait1SelfInst : ParentTrait1_t Self;
 }.
 
 Arguments mkChildTrait_t { _ }.
-Arguments ChildTrait_tChildTrait_t_parent_clause_0 { _ }.
-Arguments ChildTrait_tChildTrait_t_parent_clause_1 { _ }.
+Arguments ChildTrait_tChildTrait_t_ParentTrait0SelfInst { _ }.
+Arguments ChildTrait_tChildTrait_t_ParentTrait1SelfInst { _ }.
 
 (** [traits::test_child_trait1]: forward function
     Source: 'src/traits.rs', lines 209:0-209:56 *)
 Definition test_child_trait1
   (T : Type) (inst : ChildTrait_t T) (x : T) : result alloc_string_String_t :=
-  inst.(ChildTrait_tChildTrait_t_parent_clause_0).(ParentTrait0_t_get_name) x
+  inst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_name)
+    x
 .
 
 (** [traits::test_child_trait2]: forward function
@@ -415,9 +416,9 @@ Definition test_child_trait1
 Definition test_child_trait2
   (T : Type) (inst : ChildTrait_t T) (x : T) :
   result
-    inst.(ChildTrait_tChildTrait_t_parent_clause_0).(ParentTrait0_tParentTrait0_t_W)
+    inst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_tParentTrait0_t_W)
   :=
-  inst.(ChildTrait_tChildTrait_t_parent_clause_0).(ParentTrait0_t_get_w) x
+  inst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_w) x
 .
 
 (** [traits::order1]: forward function
@@ -432,11 +433,11 @@ Definition order1
 (** Trait declaration: [traits::ChildTrait1]
     Source: 'src/traits.rs', lines 222:0-222:35 *)
 Record ChildTrait1_t (Self : Type) := mkChildTrait1_t {
-  ChildTrait1_tChildTrait1_t_parent_clause_0 : ParentTrait1_t Self;
+  ChildTrait1_tChildTrait1_t_ParentTrait1SelfInst : ParentTrait1_t Self;
 }.
 
 Arguments mkChildTrait1_t { _ }.
-Arguments ChildTrait1_tChildTrait1_t_parent_clause_0 { _ }.
+Arguments ChildTrait1_tChildTrait1_t_ParentTrait1SelfInst { _ }.
 
 (** Trait implementation: [traits::{usize#9}]
     Source: 'src/traits.rs', lines 224:0-224:27 *)
@@ -446,7 +447,8 @@ Definition traits_ParentTrait1UsizeInst : ParentTrait1_t usize
 (** Trait implementation: [traits::{usize#10}]
     Source: 'src/traits.rs', lines 225:0-225:26 *)
 Definition traits_ChildTrait1UsizeInst : ChildTrait1_t usize := {|
-  ChildTrait1_tChildTrait1_t_parent_clause_0 := traits_ParentTrait1UsizeInst;
+  ChildTrait1_tChildTrait1_t_ParentTrait1SelfInst :=
+    traits_ParentTrait1UsizeInst;
 |}.
 
 (** Trait declaration: [traits::Iterator]
@@ -485,12 +487,13 @@ Arguments mkFromResidual_t { _ _ }.
     Source: 'src/traits.rs', lines 246:0-246:48 *)
 Record Try_t (Self : Type) := mkTry_t {
   Try_tTry_t_Residual : Type;
-  Try_tTry_t_parent_clause_0 : FromResidual_t Self Try_tTry_t_Residual;
+  Try_tTry_t_FromResidualSelftraitsTrySelfResidualInst : FromResidual_t Self
+    Try_tTry_t_Residual;
 }.
 
 Arguments mkTry_t { _ }.
 Arguments Try_tTry_t_Residual { _ }.
-Arguments Try_tTry_t_parent_clause_0 { _ }.
+Arguments Try_tTry_t_FromResidualSelftraitsTrySelfResidualInst { _ }.
 
 (** Trait declaration: [traits::WithTarget]
     Source: 'src/traits.rs', lines 252:0-252:20 *)
@@ -516,15 +519,15 @@ Arguments ParentTrait2_tParentTrait2_t_U_clause_0 { _ }.
 (** Trait declaration: [traits::ChildTrait2]
     Source: 'src/traits.rs', lines 260:0-260:35 *)
 Record ChildTrait2_t (Self : Type) := mkChildTrait2_t {
-  ChildTrait2_tChildTrait2_t_parent_clause_0 : ParentTrait2_t Self;
+  ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst : ParentTrait2_t Self;
   ChildTrait2_t_convert :
-    (ChildTrait2_tChildTrait2_t_parent_clause_0).(ParentTrait2_tParentTrait2_t_U)
+    (ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst).(ParentTrait2_tParentTrait2_t_U)
     -> result
-    (ChildTrait2_tChildTrait2_t_parent_clause_0).(ParentTrait2_tParentTrait2_t_U_clause_0).(WithTarget_tWithTarget_t_Target);
+    (ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst).(ParentTrait2_tParentTrait2_t_U_clause_0).(WithTarget_tWithTarget_t_Target);
 }.
 
 Arguments mkChildTrait2_t { _ }.
-Arguments ChildTrait2_tChildTrait2_t_parent_clause_0 { _ }.
+Arguments ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst { _ }.
 Arguments ChildTrait2_t_convert { _ }.
 
 (** Trait implementation: [traits::{u32#11}]
@@ -548,7 +551,8 @@ Definition u32_convert (x : u32) : result u32 :=
 (** Trait implementation: [traits::{u32#13}]
     Source: 'src/traits.rs', lines 272:0-272:24 *)
 Definition traits_ChildTrait2U32Inst : ChildTrait2_t u32 := {|
-  ChildTrait2_tChildTrait2_t_parent_clause_0 := traits_ParentTrait2U32Inst;
+  ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst :=
+    traits_ParentTrait2U32Inst;
   ChildTrait2_t_convert := u32_convert;
 |}.
 
@@ -566,29 +570,29 @@ Arguments CFnOnce_t_call_once { _ _ }.
 (** Trait declaration: [traits::CFnMut]
     Source: 'src/traits.rs', lines 292:0-292:37 *)
 Record CFnMut_t (Self Args : Type) := mkCFnMut_t {
-  CFnMut_tCFnMut_t_parent_clause_0 : CFnOnce_t Self Args;
+  CFnMut_tCFnMut_t_CFnOnceSelfArgsInst : CFnOnce_t Self Args;
   CFnMut_t_call_mut : Self -> Args -> result
-    (CFnMut_tCFnMut_t_parent_clause_0).(CFnOnce_tCFnOnce_t_Output);
+    (CFnMut_tCFnMut_t_CFnOnceSelfArgsInst).(CFnOnce_tCFnOnce_t_Output);
   CFnMut_t_call_mut_back : Self -> Args ->
-    (CFnMut_tCFnMut_t_parent_clause_0).(CFnOnce_tCFnOnce_t_Output) -> result
-    Self;
+    (CFnMut_tCFnMut_t_CFnOnceSelfArgsInst).(CFnOnce_tCFnOnce_t_Output) ->
+    result Self;
 }.
 
 Arguments mkCFnMut_t { _ _ }.
-Arguments CFnMut_tCFnMut_t_parent_clause_0 { _ _ }.
+Arguments CFnMut_tCFnMut_t_CFnOnceSelfArgsInst { _ _ }.
 Arguments CFnMut_t_call_mut { _ _ }.
 Arguments CFnMut_t_call_mut_back { _ _ }.
 
 (** Trait declaration: [traits::CFn]
     Source: 'src/traits.rs', lines 296:0-296:33 *)
 Record CFn_t (Self Args : Type) := mkCFn_t {
-  CFn_tCFn_t_parent_clause_0 : CFnMut_t Self Args;
+  CFn_tCFn_t_CFnMutSelfArgsInst : CFnMut_t Self Args;
   CFn_t_call_mut : Self -> Args -> result
-    (CFn_tCFn_t_parent_clause_0).(CFnMut_tCFnMut_t_parent_clause_0).(CFnOnce_tCFnOnce_t_Output);
+    (CFn_tCFn_t_CFnMutSelfArgsInst).(CFnMut_tCFnMut_t_CFnOnceSelfArgsInst).(CFnOnce_tCFnOnce_t_Output);
 }.
 
 Arguments mkCFn_t { _ _ }.
-Arguments CFn_tCFn_t_parent_clause_0 { _ _ }.
+Arguments CFn_tCFn_t_CFnMutSelfArgsInst { _ _ }.
 Arguments CFn_t_call_mut { _ _ }.
 
 (** [traits::incr_u32]: forward function
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 669c1dff..63ac307f 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -157,7 +157,7 @@ let h3
 (** Trait declaration: [traits::OfTypeBis]
     Source: 'src/traits.rs', lines 109:0-109:36 *)
 noeq type ofTypeBis_t (self t : Type0) = {
-  parent_clause_0 : toType_t t self;
+  toTypeTSelfInst : toType_t t self;
   of_type : t -> result self;
 }
 
@@ -311,23 +311,23 @@ type parentTrait1_t (self : Type0) = unit
 (** Trait declaration: [traits::ChildTrait]
     Source: 'src/traits.rs', lines 206:0-206:49 *)
 noeq type childTrait_t (self : Type0) = {
-  parent_clause_0 : parentTrait0_t self;
-  parent_clause_1 : parentTrait1_t self;
+  parentTrait0SelfInst : parentTrait0_t self;
+  parentTrait1SelfInst : parentTrait1_t self;
 }
 
 (** [traits::test_child_trait1]: forward function
     Source: 'src/traits.rs', lines 209:0-209:56 *)
 let test_child_trait1
   (t : Type0) (inst : childTrait_t t) (x : t) : result alloc_string_String_t =
-  inst.parent_clause_0.get_name x
+  inst.parentTrait0SelfInst.get_name x
 
 (** [traits::test_child_trait2]: forward function
     Source: 'src/traits.rs', lines 213:0-213:54 *)
 let test_child_trait2
   (t : Type0) (inst : childTrait_t t) (x : t) :
-  result inst.parent_clause_0.tW
+  result inst.parentTrait0SelfInst.tW
   =
-  inst.parent_clause_0.get_w x
+  inst.parentTrait0SelfInst.get_w x
 
 (** [traits::order1]: forward function
     Source: 'src/traits.rs', lines 219:0-219:59 *)
@@ -340,7 +340,7 @@ let order1
 (** Trait declaration: [traits::ChildTrait1]
     Source: 'src/traits.rs', lines 222:0-222:35 *)
 noeq type childTrait1_t (self : Type0) = {
-  parent_clause_0 : parentTrait1_t self;
+  parentTrait1SelfInst : parentTrait1_t self;
 }
 
 (** Trait implementation: [traits::{usize#9}]
@@ -350,7 +350,7 @@ let traits_ParentTrait1UsizeInst : parentTrait1_t usize = ()
 (** Trait implementation: [traits::{usize#10}]
     Source: 'src/traits.rs', lines 225:0-225:26 *)
 let traits_ChildTrait1UsizeInst : childTrait1_t usize = {
-  parent_clause_0 = traits_ParentTrait1UsizeInst;
+  parentTrait1SelfInst = traits_ParentTrait1UsizeInst;
 }
 
 (** Trait declaration: [traits::Iterator]
@@ -374,7 +374,7 @@ type fromResidual_t (self t : Type0) = unit
     Source: 'src/traits.rs', lines 246:0-246:48 *)
 noeq type try_t (self : Type0) = {
   tResidual : Type0;
-  parent_clause_0 : fromResidual_t self tResidual;
+  fromResidualSelftraitsTrySelfResidualInst : fromResidual_t self tResidual;
 }
 
 (** Trait declaration: [traits::WithTarget]
@@ -391,8 +391,9 @@ noeq type parentTrait2_t (self : Type0) = {
 (** Trait declaration: [traits::ChildTrait2]
     Source: 'src/traits.rs', lines 260:0-260:35 *)
 noeq type childTrait2_t (self : Type0) = {
-  parent_clause_0 : parentTrait2_t self;
-  convert : parent_clause_0.tU -> result parent_clause_0.tU_clause_0.tTarget;
+  parentTrait2SelfInst : parentTrait2_t self;
+  convert : parentTrait2SelfInst.tU -> result
+    parentTrait2SelfInst.tU_clause_0.tTarget;
 }
 
 (** Trait implementation: [traits::{u32#11}]
@@ -414,7 +415,7 @@ let u32_convert (x : u32) : result u32 =
 (** Trait implementation: [traits::{u32#13}]
     Source: 'src/traits.rs', lines 272:0-272:24 *)
 let traits_ChildTrait2U32Inst : childTrait2_t u32 = {
-  parent_clause_0 = traits_ParentTrait2U32Inst;
+  parentTrait2SelfInst = traits_ParentTrait2U32Inst;
   convert = u32_convert;
 }
 
@@ -428,16 +429,17 @@ noeq type cFnOnce_t (self args : Type0) = {
 (** Trait declaration: [traits::CFnMut]
     Source: 'src/traits.rs', lines 292:0-292:37 *)
 noeq type cFnMut_t (self args : Type0) = {
-  parent_clause_0 : cFnOnce_t self args;
-  call_mut : self -> args -> result parent_clause_0.tOutput;
-  call_mut_back : self -> args -> parent_clause_0.tOutput -> result self;
+  cFnOnceSelfArgsInst : cFnOnce_t self args;
+  call_mut : self -> args -> result cFnOnceSelfArgsInst.tOutput;
+  call_mut_back : self -> args -> cFnOnceSelfArgsInst.tOutput -> result self;
 }
 
 (** Trait declaration: [traits::CFn]
     Source: 'src/traits.rs', lines 296:0-296:33 *)
 noeq type cFn_t (self args : Type0) = {
-  parent_clause_0 : cFnMut_t self args;
-  call_mut : self -> args -> result parent_clause_0.parent_clause_0.tOutput;
+  cFnMutSelfArgsInst : cFnMut_t self args;
+  call_mut : self -> args -> result
+    cFnMutSelfArgsInst.cFnOnceSelfArgsInst.tOutput;
 }
 
 (** [traits::incr_u32]: forward function
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index f854da76..0aa68c5e 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -170,7 +170,7 @@ def h3
 /- Trait declaration: [traits::OfTypeBis]
    Source: 'src/traits.rs', lines 109:0-109:36 -/
 structure OfTypeBis (Self T : Type) where
-  parent_clause_0 : ToType T Self
+  ToTypeTSelfInst : ToType T Self
   of_type : T → Result Self
 
 /- [traits::h4]: forward function
@@ -327,20 +327,22 @@ structure ParentTrait1 (Self : Type) where
 /- Trait declaration: [traits::ChildTrait]
    Source: 'src/traits.rs', lines 206:0-206:49 -/
 structure ChildTrait (Self : Type) where
-  parent_clause_0 : ParentTrait0 Self
-  parent_clause_1 : ParentTrait1 Self
+  ParentTrait0SelfInst : ParentTrait0 Self
+  ParentTrait1SelfInst : ParentTrait1 Self
 
 /- [traits::test_child_trait1]: forward function
    Source: 'src/traits.rs', lines 209:0-209:56 -/
 def test_child_trait1
   (T : Type) (inst : ChildTrait T) (x : T) : Result alloc.string.String :=
-  inst.parent_clause_0.get_name x
+  inst.ParentTrait0SelfInst.get_name x
 
 /- [traits::test_child_trait2]: forward function
    Source: 'src/traits.rs', lines 213:0-213:54 -/
 def test_child_trait2
-  (T : Type) (inst : ChildTrait T) (x : T) : Result inst.parent_clause_0.W :=
-  inst.parent_clause_0.get_w x
+  (T : Type) (inst : ChildTrait T) (x : T) :
+  Result inst.ParentTrait0SelfInst.W
+  :=
+  inst.ParentTrait0SelfInst.get_w x
 
 /- [traits::order1]: forward function
    Source: 'src/traits.rs', lines 219:0-219:59 -/
@@ -353,7 +355,7 @@ def order1
 /- Trait declaration: [traits::ChildTrait1]
    Source: 'src/traits.rs', lines 222:0-222:35 -/
 structure ChildTrait1 (Self : Type) where
-  parent_clause_0 : ParentTrait1 Self
+  ParentTrait1SelfInst : ParentTrait1 Self
 
 /- Trait implementation: [traits::{usize#9}]
    Source: 'src/traits.rs', lines 224:0-224:27 -/
@@ -363,7 +365,7 @@ def traits.ParentTrait1UsizeInst : ParentTrait1 Usize := {
 /- Trait implementation: [traits::{usize#10}]
    Source: 'src/traits.rs', lines 225:0-225:26 -/
 def traits.ChildTrait1UsizeInst : ChildTrait1 Usize := {
-  parent_clause_0 := traits.ParentTrait1UsizeInst
+  ParentTrait1SelfInst := traits.ParentTrait1UsizeInst
 }
 
 /- Trait declaration: [traits::Iterator]
@@ -387,7 +389,7 @@ structure FromResidual (Self T : Type) where
    Source: 'src/traits.rs', lines 246:0-246:48 -/
 structure Try (Self : Type) where
   Residual : Type
-  parent_clause_0 : FromResidual Self Residual
+  FromResidualSelftraitsTrySelfResidualInst : FromResidual Self Residual
 
 /- Trait declaration: [traits::WithTarget]
    Source: 'src/traits.rs', lines 252:0-252:20 -/
@@ -403,8 +405,9 @@ structure ParentTrait2 (Self : Type) where
 /- Trait declaration: [traits::ChildTrait2]
    Source: 'src/traits.rs', lines 260:0-260:35 -/
 structure ChildTrait2 (Self : Type) where
-  parent_clause_0 : ParentTrait2 Self
-  convert : parent_clause_0.U → Result parent_clause_0.U_clause_0.Target
+  ParentTrait2SelfInst : ParentTrait2 Self
+  convert : ParentTrait2SelfInst.U → Result
+    ParentTrait2SelfInst.U_clause_0.Target
 
 /- Trait implementation: [traits::{u32#11}]
    Source: 'src/traits.rs', lines 264:0-264:23 -/
@@ -427,7 +430,7 @@ def U32.convert (x : U32) : Result U32 :=
 /- Trait implementation: [traits::{u32#13}]
    Source: 'src/traits.rs', lines 272:0-272:24 -/
 def traits.ChildTrait2U32Inst : ChildTrait2 U32 := {
-  parent_clause_0 := traits.ParentTrait2U32Inst
+  ParentTrait2SelfInst := traits.ParentTrait2U32Inst
   convert := U32.convert
 }
 
@@ -440,15 +443,16 @@ structure CFnOnce (Self Args : Type) where
 /- Trait declaration: [traits::CFnMut]
    Source: 'src/traits.rs', lines 292:0-292:37 -/
 structure CFnMut (Self Args : Type) where
-  parent_clause_0 : CFnOnce Self Args
-  call_mut : Self → Args → Result parent_clause_0.Output
-  call_mut_back : Self → Args → parent_clause_0.Output → Result Self
+  CFnOnceSelfArgsInst : CFnOnce Self Args
+  call_mut : Self → Args → Result CFnOnceSelfArgsInst.Output
+  call_mut_back : Self → Args → CFnOnceSelfArgsInst.Output → Result Self
 
 /- Trait declaration: [traits::CFn]
    Source: 'src/traits.rs', lines 296:0-296:33 -/
 structure CFn (Self Args : Type) where
-  parent_clause_0 : CFnMut Self Args
-  call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output
+  CFnMutSelfArgsInst : CFnMut Self Args
+  call_mut : Self → Args → Result
+    CFnMutSelfArgsInst.CFnOnceSelfArgsInst.Output
 
 /- [traits::incr_u32]: forward function
    Source: 'src/traits.rs', lines 300:0-300:30 -/