diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index dfb8af8b33ba4ce5562bb4067da9d3a06f89a924..11a8f4967fec1292d011a30001f79b89e34a37eb 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -397,7 +397,9 @@ Hint Resolve tctx_extract_split_own_prod2 tctx_extract_split_uniq_prod2
      | 60 : lrust_typing.
 
 (* We make sure that this is applied after everything. *)
-Hint Resolve tctx_extract_merge_own_prod tctx_extract_merge_uniq_prod
-             tctx_extract_merge_shr_prod | 150 : lrust_typing.
+Hint Resolve tctx_extract_merge_own_prod2 tctx_extract_merge_uniq_prod2
+             tctx_extract_merge_shr_prod2 tctx_extract_merge_own_prod
+             tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod
+     | 150 : lrust_typing.
 
 Hint Unfold extract_tyl : lrust_typing.