From 17aaad5af629ada4ecaa8bfb75a0c416c937ec70 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 22 Nov 2022 13:56:17 +0100 Subject: [PATCH] Adapt to coq/coq#16743 (fix incomplete checking of unsolved holes) Alternatively we could define `exploit` as a Tactic Notation taking open_constr or uconstr (the problem is that arguments to a non-notation Ltac get interpreted as constr which doesn't allow holes, but in this case a hole gets solved by typeclass inference leaving a new hole behing, and due to the bug the new hole isn't detected). --- cfrontend/Ctypes.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 39117959d9..8da714cd36 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -1902,7 +1902,7 @@ Theorem link_match_program_gen: exists tp, link tp1 tp2 = Some tp /\ match_program p tp. Proof. intros until p; intros L [M1 T1] [M2 T2]. - exploit link_linkorder; eauto. intros [LO1 LO2]. + destruct (link_linkorder _ _ _ L) as [LO1 LO2]. Local Transparent Linker_program. simpl in L; unfold link_program in L. destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate.