From 6106e043c8a13bf882d2227b3ee80a108305d8df Mon Sep 17 00:00:00 2001 From: Xia Li-yao Date: Thu, 25 Mar 2021 12:21:14 -0400 Subject: Do not depend on projection parameter names (#388) coq/coq#13852 fixes an oddity in the automatically-generated names for projection parameters. There was one place in CompCert where one of these automatically-generated names was used. This commit avoids using this name. --- common/Separation.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/common/Separation.v b/common/Separation.v index bf134a18..dcd07ca8 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -870,7 +870,7 @@ Proof. exists j', vres2, m2'; intuition auto. split; [|split]. - exact INJ'. -- apply m_invar with (m0 := m2). +- apply (m_invar _ m2). + apply globalenv_inject_incr with j m1; auto. + eapply Mem.unchanged_on_implies; eauto. intros; red; intros; red; intros. -- cgit