From 718290e12fb90f7ab16ed4eee1636f8247955fe2 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Thu, 1 Dec 2016 21:23:59 +0100
Subject: [PATCH] Remove a warning about a [ty_of_st], better compatibility fix
 in [perm_incl.v].

---
 theories/typing/perm_incl.v | 24 ++++--------------------
 theories/typing/type.v      |  4 +++-
 2 files changed, 7 insertions(+), 21 deletions(-)

diff --git a/theories/typing/perm_incl.v b/theories/typing/perm_incl.v
index 5a78834f..a29d8cb0 100644
--- a/theories/typing/perm_incl.v
+++ b/theories/typing/perm_incl.v
@@ -176,35 +176,19 @@ 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 //=.
-      apply perm_sep_proper.
+      injection Hlen; intro Hlen'. rewrite perm_split_own_prod2 IH //.
+      set (q1l := q1::ql). cbn[combine_offs combine foldr]. 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.
+      + 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.
+        * etrans. apply IHl. by injection Hlen. do 3 f_equiv. lia.
   Qed.
 
   Lemma perm_split_uniq_bor_prod2 ty1 ty2 κ ν :
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 506470f9..398506c6 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -64,7 +64,7 @@ Record simple_type `{iris_typeG Σ} :=
     st_own_persistent tid vl : PersistentP (st_own tid vl) }.
 Global Existing Instance st_own_persistent.
 
-Program Coercion ty_of_st (st : simple_type) : type :=
+Program Definition ty_of_st (st : simple_type) : type :=
   {| ty_size := st.(st_size); ty_dup := true;
      ty_own := st.(st_own);
 
@@ -106,6 +106,8 @@ Qed.
 
 End type.
 
+Coercion ty_of_st : simple_type >-> type.
+
 Hint Extern 0 (Is_true _.(ty_dup)) =>
   exact I || assumption : typeclass_instances.
 
-- 
GitLab