From e24a773588ee50bb3033fc1dcb3f5ce567471f2e Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 1 Dec 2016 17:55:27 +0100
Subject: [PATCH] Revert "Coq 8.6 compatibility"

This reverts commit 3ddb6014c152fe1006a762da0f9d5ee7e11019a1.
I did not intend to push this to master, sorry :/
---
 theories/lang/races.v           |  2 +-
 theories/lifetime/frac_borrow.v |  2 +-
 theories/typing/perm_incl.v     | 27 ++++++---------------------
 3 files changed, 8 insertions(+), 23 deletions(-)

diff --git a/theories/lang/races.v b/theories/lang/races.v
index 5d78a388..43916151 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -201,7 +201,7 @@ Proof.
 
   destruct Ha1 as [[]|[]| | |], Ha2 as [[]|[]| | |]=>//=; simpl in *;
     repeat match goal with
-    | H : _ = Na1Ord → _ |- _ => specialize (H (eq_refl Na1Ord)) || clear H
+    | H : _ = Na1Ord → _ |- _ => specialize (H (reflexivity Na1Ord)) || clear H
     | H : False |- _ => destruct H
     | H : ∃ _, _ |- _ => destruct H
     end;
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 0ae322ab..b77f8b33 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -84,7 +84,7 @@ Section frac_bor.
     { change (qΦ + qq ≤ 1)%Qc in Hval. apply Qp_eq in HqΦq'. simpl in Hval, HqΦq'.
       rewrite <-HqΦq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
       destruct Hval as [Hval|Hval].
-      by left; apply ->Qclt_minus_iff. right; apply Qp_eq, Qc_is_canon. by rewrite Hval. }
+      by left; apply ->Qclt_minus_iff. by right; apply Qp_eq, Qc_is_canon. }
     - assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. }
       iDestruct "Hq'κ" as "[Hq'qκ Hqκ]".
       iMod ("Hclose'" with "[HqΦ HΦqΦ Hown Hq'qκ]") as "Hqκ2".
diff --git a/theories/typing/perm_incl.v b/theories/typing/perm_incl.v
index 5a78834f..4e58a261 100644
--- a/theories/typing/perm_incl.v
+++ b/theories/typing/perm_incl.v
@@ -176,35 +176,20 @@ Section props.
       { apply Qcplus_pos_nonneg. apply Qp_prf. clear. induction ql. done.
         apply Qcplus_nonneg_nonneg. apply Qclt_le_weak, Qp_prf. done. }
       assert (q = q0 + mk_Qp _ Hpos)%Qp as ->. by by apply Qp_eq; rewrite -Hq.
-      injection Hlen; intro Hlen'. rewrite perm_split_own_prod2 IH //=.
+      injection Hlen; intro Hlen'. rewrite perm_split_own_prod2 IH //.
       apply perm_sep_proper.
       + rewrite /has_type /sep /=.
         destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "_ H/=";
         (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]");
         (try by auto); by rewrite shift_loc_0.
-      + (* FIXME RJ: These two 'change' make the goal look like it did in Coq 8.5
-           I found no way to reproduce the magic 8.5 did. *)
-        change ( foldr
-                   (λ (qtyoffs : Qp * (type * nat)) (acc : perm),
-                    ν +ₗ #(ty_size ty0) +ₗ #((qtyoffs.2).2) ◁ own (qtyoffs.1) ((qtyoffs.2).1) ∗ acc) 
-                   ⊤ (combine (q1 :: ql) (combine_offs tyl 0))
-                   ⇔ foldr
-                   (λ (qtyoffs : Qp * (type * nat)) (acc : perm), ν +ₗ #((qtyoffs.2).2) ◁ own (qtyoffs.1) ((qtyoffs.2).1) ∗ acc)
-                   ⊤ (combine (q1 :: ql) (combine_offs tyl (0 + ty_size ty0)))).
-        cut (length tyl = length (q1 :: ql)); last done. clear. revert tyl.
-        generalize 0%nat. induction (q1 :: ql)=>offs -[|ty tyl] Hlen //=.
+      + cut (length tyl = length (q1 :: ql)); last done. clear. revert tyl.
+        generalize 0%nat. induction (q1 :: ql)=>offs -[|ty tyl] Hlen //.
         apply perm_sep_proper.
         * rewrite /has_type /sep /=.
           destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "_ H/=";
-          (try by iDestruct "H" as "[]"); [|]; by rewrite shift_loc_assoc_nat (comm plus).
-        * change ( foldr
-                     (λ (qtyoffs : Qp * (type * nat)) (acc : perm),
-                      ν +ₗ #(ty_size ty0) +ₗ #((qtyoffs.2).2) ◁ own (qtyoffs.1) ((qtyoffs.2).1) ∗ acc) 
-                     ⊤ (combine l (combine_offs tyl (offs + ty_size ty)))
-                     ⇔ foldr
-                     (λ (qtyoffs : Qp * (type * nat)) (acc : perm), ν +ₗ #((qtyoffs.2).2) ◁ own (qtyoffs.1) ((qtyoffs.2).1) ∗ acc)
-                     ⊤ (combine l (combine_offs tyl (offs + ty_size ty0 + ty_size ty)))).
-          etransitivity. apply IHl. by injection Hlen. do 3 f_equiv. lia.
+          (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]");
+          (try by auto); by rewrite shift_loc_assoc_nat (comm plus).
+        * etransitivity. apply IHl. by injection Hlen. do 3 f_equiv. lia.
   Qed.
 
   Lemma perm_split_uniq_bor_prod2 ty1 ty2 κ ν :
-- 
GitLab