From 34abc914b6c560d594fca852ded69570332ded04 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Feb 2020 17:59:27 +0100
Subject: [PATCH] Tidy up Coqdoc.

---
 theories/heap_lang/array.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index c5edacc8e..deacf72e8 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -79,7 +79,7 @@ Proof.
   rewrite drop_insert; last by lia. done.
 Qed.
 
-(** Allocation *)
+(** * Rules for allocation *)
 Lemma mapsto_seq_array l q v n :
   ([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦{q} v) -∗
   l ↦∗{q} replicate n v.
@@ -133,7 +133,7 @@ Proof.
   iApply twp_allocN_vec; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
 Qed.
 
-(** Access to array elements *)
+(** * Rules for accessing array elements *)
 Lemma twp_load_offset s E l q off vs v :
   vs !! off = Some v →
   [[{ l ↦∗{q} vs }]] ! #(l +ₗ off) @ s; E [[{ RET v; l ↦∗{q} vs }]].
-- 
GitLab