From 5be9ae2235b16239f023a36679b7d515dd774c68 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 28 Nov 2022 11:45:58 +0100 Subject: Fix incomplete checking of unsolved holes (#465) Adaptation to https://github.com/coq/coq/pull/16743 --- cfrontend/Ctypes.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 39117959..8da714cd 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. -- cgit