From cb16e4bd3c5b000e9774539541a52008cf8db751 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 8 Aug 2016 10:58:57 +0200
Subject: [PATCH] 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.
---
 program_logic/adequacy.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index f8927d9da..77f42d3dc 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -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".
-- 
GitLab