Commit cb16e4bd authored by Robbert Krebbers's avatar Robbert Krebbers

Fix compatibility with ssreflect 1.6 (which is used on the CI machine).

This is probably due to a bug in the rewrite of ssreflect 1.6 which has
been fixed in ssreflect master.
parent 340afd90
Pipeline #2565 passed with stage
in 4 minutes and 18 seconds
......@@ -94,7 +94,7 @@ Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
world σ1 WP e1 {{ v, φ v }} wptp t1
Nat.iter (S (S n)) (λ P, |=r=> P) ( φ v2).
Proof.
intros. rewrite wptp_steps // (Nat_iter_S_r (S n)); []. apply: rvs_iter_mono.
intros. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono.
iDestruct 1 as (e2 t2') "(% & (Hw & HE & _) & H & _)"; simplify_eq.
iDestruct (wp_value_inv with "H") as "H". rewrite pvs_eq /pvs_def.
iVs ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
......@@ -114,7 +114,7 @@ Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
world σ1 WP e1 {{ Φ }} wptp t1
Nat.iter (S (S n)) (λ P, |=r=> P) ( (is_Some (to_val e2) reducible e2 σ2)).
Proof.
intros ? He2. rewrite wptp_steps // (Nat_iter_S_r (S n)); apply: rvs_iter_mono.
intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono.
iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq.
apply elem_of_cons in He2 as [<-|?]; first (iApply wp_safe; by iFrame "Hw H").
iApply wp_safe. iFrame "Hw".
......
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