diff --git a/opam b/opam
index d25fc9d55c74342277ee7c2303adf1bb1367073d..ca90434e6208bae52e3a7d244b7d1d133db5ab5a 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
 depends: [
-  "coq-iris" { (= "dev.2020-10-20.2.c65b38ea") | (= "dev") }
+  "coq-iris" { (= "dev.2020-10-30.0.6dba10c0") | (= "dev") }
 ]
diff --git a/theories/lib/Q.v b/theories/lib/Q.v
index 1f0e5353867e3a6c4e29fabcbbc82f3a4c195f53..c1cc5b1f161b14e3668affce14d0ab13b1725fc1 100644
--- a/theories/lib/Q.v
+++ b/theories/lib/Q.v
@@ -5,8 +5,8 @@ Lemma Q_plus_nonneg p q : (0 < p)%Q → (0 < q)%Q → (0 < p + q)%Q.
 Proof.
   intros. apply Qlt_trans with p=> //. by rewrite -{1}(Qplus_0_r p) Qplus_lt_r.
 Qed.
-Lemma Q_div_nonneg p n : (0 < p)%Q → (0 < p / Zpos n)%Q.
-Proof. intros. by apply Qlt_shift_div_l. Qed.
+Lemma Q_div_nonneg p q : (0 < p)%Q → (0 < q)%Q → (0 < p / q)%Q.
+Proof. intros. by apply Qlt_shift_div_l; rewrite ?Qmult_0_l. Qed.
 
 Instance Q_eq_dec : EqDecision Q.
 Proof. solve_decision. Defined.
@@ -15,21 +15,15 @@ Proof. intros pq; apply Qeq_dec. Defined.
 Instance Q_lt_dec : RelDecision Qlt.
 Proof. refine (λ p q, cast_if (Qlt_le_dec p q)); auto using Qle_not_lt. Defined.
 
-Fixpoint Pos_to_pred_nat (p : positive) : nat :=
-  match p with
-  | xH => 0
-  | xO p => S (2 * Pos_to_pred_nat p)
-  | xI p => S (S (2 * Pos_to_pred_nat p))
-  end.
+Definition Qp_to_Q (q : Qp) : Q := Qp_to_Qc q.
 
 Definition Q_to_Qp (q : Q) : Qp :=
   match Qred q with
-  | Qmake (Zpos n) 1 => Nat.iter (Pos_to_pred_nat n) (λ n, 1 + n) 1
-  | Qmake (Zpos n) d => Nat.iter (Pos_to_pred_nat n) (λ n, 1 + n) 1 / d
+  | Qmake (Zpos n) 1 => pos_to_Qp n
+  | Qmake (Zpos n) d => pos_to_Qp n / pos_to_Qp d
   | _ => 1 (* dummy *)
   end%Qp.
 Arguments Q_to_Qp !_ /.
-Arguments Pos.mul !_ !_ /.
 Local Arguments Q_to_Qp : simpl never.
 
 Lemma Q_to_Qp_le_0 q : ¬(0 < q)%Q → Q_to_Qp q = 1%Qp.
@@ -40,46 +34,39 @@ Qed.
 Lemma Q_to_Qp_1 : Q_to_Qp 1 = 1%Qp.
 Proof. done. Qed.
 
-Lemma Pos_to_pred_Q_spec p :
-  Nat.iter (Pos_to_pred_nat p) (λ n, 1 + n)%Qp 1%Qp == Qmake (Z.pos p) 1.
-Proof.
-  cut (∀ q,
-    Nat.iter (Pos_to_pred_nat p) (λ n, 1 + n)%Qp q == Qmake (Z.pos p) 1 + q - 1).
-  { intros ->. rewrite /Qeq /=; lia. }
-  induction p as [p IH|p IH|]=> q' //=.
-  - rewrite !Qred_correct !Nat_iter_add !IH /=. rewrite /Qeq /=; lia.
-  - rewrite !Qred_correct !Nat_iter_add !IH /=. rewrite /Qeq /=; lia.
-  - rewrite /Qeq /=; lia.
-Qed.
+Lemma Qp_to_Q_nonneg q : (0 < Qp_to_Q q)%Q.
+Proof. by destruct q. Qed.
 
-(* this (Qp_car (Q_to_Qp q)) : Q) == q *)
-Lemma Q_of_to_Qp (q : Q) : (0 < q)%Q → (Q_to_Qp q : Q) == q.
+Lemma Q_of_to_Qp q : (0 < q)%Q → Qp_to_Q (Q_to_Qp q) == q.
 Proof.
   rewrite -{1 3}(Qred_correct q) /Q_to_Qp.
-  destruct (Qred q) as [[|n|n] d]=> ? //=.
-  destruct d as [d|d|]=> //=.
-  - by rewrite Pos_to_pred_Q_spec !Qred_correct /Qeq /= Z.mul_1_r.
-  - by rewrite Pos_to_pred_Q_spec !Qred_correct /Qeq /= Z.mul_1_r.
-  - by rewrite Pos_to_pred_Q_spec.
+  destruct (Qred q) as [[|n|n] [d|d|]]=> ? //=.
+  - by rewrite Qmake_Qdiv /Qp_to_Q /pos_to_Qp /Qc_of_Z /= !Qred_correct.
+  - by rewrite Qmake_Qdiv /Qp_to_Q /pos_to_Qp /Qc_of_Z /= !Qred_correct.
 Qed.
 
-(* Q_to_Qp (this (Qp_car q) : Q) = q *)
-Lemma Q_to_of_Qp (q : Qp) : Q_to_Qp (q : Q) = q.
-Proof. apply Qp_eq, Qc_is_canon. destruct q as [n d]. by rewrite Q_of_to_Qp. Qed.
+Lemma Q_to_of_Qp (q : Qp) : Q_to_Qp (Qp_to_Q q) = q.
+Proof. apply Qp_to_Qc_inj_iff, Qc_is_canon, Q_of_to_Qp, Qp_to_Q_nonneg. Qed.
 
 Instance Q_to_Qp_proper : Proper (Qeq ==> (=)) Q_to_Qp.
 Proof. rewrite /Q_to_Qp. by intros p p' ->%Qred_complete. Qed.
+Instance Qp_to_Q_inj : Inj (=) Qeq Qp_to_Q.
+Proof. intros p q Hpq. by rewrite -(Q_to_of_Qp p) -(Q_to_of_Qp q) Hpq. Qed.
 
-Lemma Q_to_Qp_plus p q :
+Lemma Qp_to_Q_add p q : Qp_to_Q (p + q) == Qp_to_Q p + Qp_to_Q q.
+Proof. destruct p, q. by rewrite /Qp_to_Q /= Qred_correct. Qed.
+Lemma Qp_to_Q_div p q : Qp_to_Q (p / q) == Qp_to_Q p / Qp_to_Q q.
+Proof. destruct p, q. by rewrite /Qp_to_Q /= !Qred_correct. Qed.
+
+Lemma Q_to_Qp_add p q :
   (0 < p)%Q → (0 < q)%Q → Q_to_Qp (p + q) = (Q_to_Qp p + Q_to_Qp q)%Qp.
 Proof.
   intros. assert (0 < p + q)%Q by eauto using Q_plus_nonneg.
-  apply Qp_eq, Qc_is_canon. by rewrite /= Qred_correct !Q_of_to_Qp.
+  apply (inj Qp_to_Q). by rewrite Qp_to_Q_add !Q_of_to_Qp.
 Qed.
-
-Lemma Q_to_Qp_div q p :
-  (0 < q)%Q → Q_to_Qp (q / Zpos p) = (Q_to_Qp q / p)%Qp.
+Lemma Q_to_Qp_div p q :
+  (0 < p)%Q → (0 < q)%Q → Q_to_Qp (p / q) = (Q_to_Qp p / Q_to_Qp q)%Qp.
 Proof.
-  intros. assert (0 < q / Z.pos p)%Q by eauto using Q_div_nonneg.
-  apply Qp_eq, Qc_is_canon. by rewrite /= !Qred_correct !Q_of_to_Qp.
+  intros. assert (0 < p / q)%Q by eauto using Q_div_nonneg.
+  apply (inj Qp_to_Q). by rewrite Qp_to_Q_div !Q_of_to_Qp.
 Qed.
diff --git a/theories/vcgen/denv.v b/theories/vcgen/denv.v
index 0bd9c1aa488a54349fc5228f1a37a6a326f3175f..37f8563da74039afc1062b3d5699da055839aa64 100644
--- a/theories/vcgen/denv.v
+++ b/theories/vcgen/denv.v
@@ -157,8 +157,8 @@ Definition denv_delete_frac_2 (i : nat)
 Definition denv_delete_full_2 (i : nat)
     (ms : list denv) (m : denv) : option (list denv * denv * dval) :=
   match denv_delete_full_stack_aux i ms, denv_delete_full_aux i m with
-  | None, Some (m', q, dv) => guard (q = 1)%Qp; Some (ms, m', dv)
-  | Some (ms', q, dv), None => guard (q = 1)%Qp; Some (ms', m, dv)
+  | None, Some (m', q, dv) => guard (q = 1)%Q; Some (ms, m', dv)
+  | Some (ms', q, dv), None => guard (q = 1)%Q; Some (ms', m, dv)
   | Some (ms', q1, dv), Some (m', q2, _) =>
      guard (q1 + q2 = 1)%Q; Some (ms', m', dv)
   | _, _ => None
@@ -598,7 +598,7 @@ Section denv.
     - rewrite denv_interp_singleton_aux. iIntros "[_ $]".
     - destruct i as [|i].
       + iIntros "[[H1 $] H2] /=".
-        rewrite Q_to_Qp_plus //. iDestruct (mapsto_value_agree with "H1 H2") as %->.
+        rewrite Q_to_Qp_add //. iDestruct (mapsto_value_agree with "H1 H2") as %->.
         by iCombine "H1 H2" as "H".
       + iIntros "[[$ H1] H2]". setoid_rewrite Nat.add_succ_r; simpl.
         iApply ("IH" $! _ (S _)); auto with iFrame.
@@ -628,7 +628,7 @@ Section denv.
     { iIntros "[$ _]". }
     iIntros "[[Hl1 H1] [Hl2 H2]] /=". iSplitL "Hl1 Hl2".
     { destruct dio1 as [[x1 q1 dv1]|], dio2 as [[x2 q2 dv2]|]=> //=; simpl in *; destruct_and?.
-      rewrite Q_to_Qp_plus //. iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
+      rewrite Q_to_Qp_add //. iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
       by iCombine "Hl1 Hl2" as "Hl". }
     setoid_rewrite Nat.add_succ_r; simpl.
     iApply ("IH" $! _ (S _)); auto with iFrame.
@@ -651,7 +651,7 @@ Section denv.
     { by destruct i. }
     destruct i as [|i]; simpl in *.
     - destruct dio as [[x q' dv']|]; simplify_option_eq; destruct_and?.
-      iIntros "[[Hl1 Hl2] $] /=". rewrite -!Q_to_Qp_div //. iFrame.
+      iIntros "[[Hl1 Hl2] $] /=". rewrite !Q_to_Qp_div //. iFrame.
     - destruct (denv_delete_frac i m) as [[[mf q'] dv']|] eqn:Hdenv; simplify_eq/=.
       iIntros "[$ Hm]". setoid_rewrite Nat.add_succ_r; simpl.
       by iApply ("IH" $! _ (S _)).
@@ -789,7 +789,7 @@ Section denv.
         iApply (denv_stack_interp_wand with "IH"); iIntros "Hl Hm".
         rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux /=; last done.
         iDestruct "Hm" as "[$ Hl2]".
-        rewrite Q_to_Qp_plus; eauto using denv_wf_frac_wf_delete_full_aux,
+        rewrite Q_to_Qp_add; eauto using denv_wf_frac_wf_delete_full_aux,
           denv_wf_frac_wf_delete_full_stack_aux.
         iDestruct (mapsto_value_agree with "Hl Hl2") as %->.
         iCombine "Hl Hl2" as "$".
@@ -836,7 +836,7 @@ Section denv.
       iIntros "[$ Hl2]".
       iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
       iCombine "Hl1 Hl2" as "Hl".
-      rewrite -Q_to_Qp_plus; eauto using denv_wf_frac_wf_delete_full_aux,
+      rewrite -Q_to_Qp_add; eauto using denv_wf_frac_wf_delete_full_aux,
         denv_wf_frac_wf_delete_full_stack_aux.
       rewrite (_ : (_ + _)%Q = 1%Q) //.
     - iApply denv_stack_interp_wand;
diff --git a/theories/vcgen/proofmode.v b/theories/vcgen/proofmode.v
index d4afccb53d236cb324a5c8627a7c99e9f1b453ef..8680d65512dbedde4aad1342f088c9fb76c1a755 100644
--- a/theories/vcgen/proofmode.v
+++ b/theories/vcgen/proofmode.v
@@ -42,7 +42,7 @@ Section tactics.
   Proof. by split. Qed.
   Global Instance prop_into_denv_mapsto E E' E'' cl i lv q v dv m :
     LocLookup E E' cl i → IntoDVal E' E'' v dv →
-    PropIntoDEnv E E'' (cl ↦C[lv]{q} v) emp m (denv_insert i lv q dv m).
+    PropIntoDEnv E E'' (cl ↦C[lv]{q} v) emp m (denv_insert i lv (Qp_to_Q q) dv m).
   Proof.
     intros [??] [-> ? HE']. split; last by etrans.
     - iIntros (?) "[??]". iSplit=> //.