Some hints were missing.

6a821906 · Jacques-Henri Jourdan · b7505585 · 6a821906
Commit 6a821906 authored 8 years ago by Jacques-Henri Jourdan
--- 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.