diff options
| author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2022-11-28 11:45:58 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-11-28 11:45:58 +0100 |
| commit | 5be9ae2235b16239f023a36679b7d515dd774c68 (patch) | |
| tree | f90ecb4045c08a0d92a086468869261d4f61d9bc | |
| parent | db8a63f28efbdc3bcbe170320bef4102be3b13da (diff) | |
| download | compcert-5be9ae2235b16239f023a36679b7d515dd774c68.tar.gz compcert-5be9ae2235b16239f023a36679b7d515dd774c68.zip | |
Fix incomplete checking of unsolved holes (#465)
Adaptation to https://github.com/coq/coq/pull/16743
| -rw-r--r-- | cfrontend/Ctypes.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |