From af8d4175ad1ee0fdc9d663db2ff7644e2307a7ec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 Feb 2016 21:01:48 +0100
Subject: [PATCH] Fix typo in comments and turn them into Coqdoc.

---
 program_logic/pviewshifts.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index a60649647..03ce44e37 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.
-- 
GitLab