Merge branch 'coq-8.6' into 'master'

Coq 8.6

These are the changes necessary to make this compatible with Coq 8.6. Most of the changes are fine (and of the category "no idea why this worked in 8.5" or "the statement of a lemma changed in the 8.6 libs"), except for the horribleness in perm_incl.v. I played around a little but found no good way to restore the term into the state Coq 8.5 put it in -- and the goals I end up in otherwise (if I just remove the `change`) look fairly unsolvable.

Cc @jjourdan @robbertkrebbers

See merge request !3

theories/lang/races.v

@@ -201,7 +201,7 @@ Proof.
 
   destruct Ha1 as [[]|[]| | |], Ha2 as [[]|[]| | |]=>//=; simpl in *;
     repeat match goal with
-    | H : _ = Na1Ord → _ |- _ => specialize (H (reflexivity Na1Ord)) || clear H
+    | H : _ = Na1Ord → _ |- _ => specialize (H (eq_refl Na1Ord)) || clear H
     | H : False |- _ => destruct H
     | H : ∃ _, _ |- _ => destruct H
     end;

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. by right; apply Qp_eq, Qc_is_canon. }
+      by left; apply ->Qclt_minus_iff. right; apply Qp_eq, Qc_is_canon. by rewrite Hval. }
     - 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".

theories/typing/perm_incl.v

@@ -177,19 +177,18 @@ Section props.
         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.
+      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.
       + cut (length tyl = length (q1 :: ql)); last done. clear. revert tyl.
-        generalize 0%nat. induction (q1 :: ql)=>offs -[|ty tyl] Hlen //.
+        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 "[]"); (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.
+          (try by iDestruct "H" as "[]"); [|]; by rewrite shift_loc_assoc_nat (comm plus).
+        * etrans. apply IHl. by injection Hlen. do 3 f_equiv. lia.
   Qed.
 
   Lemma perm_split_uniq_bor_prod2 ty1 ty2 κ ν :

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.