Commit 43c867da authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Fix bug when building with coq 8.7.2

parent 7df95753
Pipeline #7249 failed with stage
in 21 minutes and 38 seconds
......@@ -697,13 +697,13 @@ Proof. by rewrite affine_equiv and_elim_l. Qed.
Lemma sep_affine_3 P Q: (P Q) (P Q).
Proof.
- unseal; constructor.
intros n x y ?? ((x1&x2&y1&y2&Hx&Hy&(?&Hy1)&HQ)&Hempty).
assert (y2 {n} ) as Hy2.
{ rewrite -Hempty Hy Hy1 left_id //=. }
exists x1, x2, y1, y2. split_and!; auto.
* split; auto.
* split; auto.
unseal; constructor.
intros n x y ?? ((x1&x2&y1&y2&Hx&Hy&(?&Hy1)&HQ)&Hempty).
assert (y2 {n} ) as Hy2.
{ rewrite -Hempty Hy Hy1 left_id //=. }
exists x1, x2, y1, y2. split_and!; auto.
* split; auto.
* split; auto.
Qed.
Lemma persistent_intro' P Q : (uPred_persistent P Q) uPred_persistent P uPred_persistent Q.
......
Supports Markdown
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