diff options
| author | Xia Li-yao <Lysxia@users.noreply.github.com> | 2021-03-25 12:21:14 -0400 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-25 17:21:14 +0100 |
| commit | 6106e043c8a13bf882d2227b3ee80a108305d8df (patch) | |
| tree | 4ee694780cb8793cc8c9608b0299a447f6ba02d7 /common | |
| parent | 6bf310dd678285dc193798e89fc2c441d8430892 (diff) | |
| download | compcert-kvx-6106e043c8a13bf882d2227b3ee80a108305d8df.tar.gz compcert-kvx-6106e043c8a13bf882d2227b3ee80a108305d8df.zip | |
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.
Diffstat (limited to 'common')
| -rw-r--r-- | common/Separation.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |