Unverified Commit 6106e043 authored by Xia Li-yao's avatar Xia Li-yao Committed by GitHub
Browse files

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.
parent 6bf310dd
......@@ -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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment