diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index a60649647f97518764a47e51576b7b32ffb46305..03ce44e374e46f50e2e731e6132f9fc7c825356b 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -125,7 +125,7 @@ Proof.
   by split; [by exists i; split; rewrite /uPred_holds /=|].
 Qed.
 
-(* Derived rules *)
+(** * Derived rules *)
 Opaque uPred_holds.
 Import uPred.
 Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2).
@@ -158,10 +158,10 @@ Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
   P ⊑ Q → pvs E1' E2' P ⊑ pvs E1 E2 Q.
 Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.
 
-(* It should be possible to give a stronger version of this rule
+(** It should be possible to give a stronger version of this rule
    that does not force the conclusion view shift to have twice the
    same mask. However, even expressing the side-conditions on the
-   mask becomes really ugly then, and we have now found an instance
+   mask becomes really ugly then, and we have not found an instance
    where that would be useful. *)
 Lemma pvs_trans3 E1 E2 Q :
   E2 ⊆ E1 → pvs E1 E2 (pvs E2 E2 (pvs E2 E1 Q)) ⊑ pvs E1 E1 Q.