Update the extraction

3 files changed, 15 insertions, 2 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index a73bf0fd..8ad8a18d 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2416,7 +2416,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
    * Extract the items
    *)
 
-  (* The parent clauses - we retrieve those from the impl_ref *)
+  (* The parent clauses *)
   let trait_decl_id = impl.impl_trait.trait_decl_id in
   TraitClauseId.iteri
     (fun clause_id trait_ref ->
@@ -2426,7 +2426,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
         extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref
       in
       extract_trait_impl_item ctx fmt item_name ty)
-    impl.impl_trait.decl_generics.trait_refs;
+    impl.parent_trait_refs;
 
   (* The constants *)
   List.iter
diff --git a/tests/lean/Traits/Funs.lean b/tests/lean/Traits/Funs.lean
index 156ef1e0..6a2834ff 100644
--- a/tests/lean/Traits/Funs.lean
+++ b/tests/lean/Traits/Funs.lean
@@ -227,6 +227,15 @@ def order1
   :=
   Result.ret ()
 
+/- Trait implementation: [traits::usize::{9}] -/
+def usize.ParentTrait1Inst : ParentTrait1 Usize := {
+}
+
+/- Trait implementation: [traits::usize::{10}] -/
+def usize.ChildTrait1Inst : ChildTrait1 Usize := {
+  parent_clause_0 := usize.ParentTrait1Inst
+}
+
 /- [traits::map_option]: forward function -/
 def map_option
   (T F : Type) (inst : core.ops.function.Fn F T) (x : Option T) (f0 : F) :
diff --git a/tests/lean/Traits/Types.lean b/tests/lean/Traits/Types.lean
index e325da6f..20af9cb1 100644
--- a/tests/lean/Traits/Types.lean
+++ b/tests/lean/Traits/Types.lean
@@ -72,6 +72,10 @@ structure ChildTrait (Self : Type) where
   parent_clause_0 : ParentTrait0 Self
   parent_clause_1 : ParentTrait1 Self
 
+/- Trait declaration: [traits::ChildTrait1] -/
+structure ChildTrait1 (Self : Type) where
+  parent_clause_0 : ParentTrait1 Self
+
 /- Trait declaration: [traits::Iterator] -/
 structure Iterator (Self : Type) where
   Item : Type