From 6a8219064eae886e9a28fe302a1c98736422077e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 6 Jan 2017 00:24:31 +0100
Subject: [PATCH] Some hints were missing.
---
theories/typing/product_split.v | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index dfb8af8b..11a8f496 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.
--
GitLab