From 6db5fb8dade4df7970d62245c2723e0e765d81d4 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 2 Apr 2020 14:41:43 +0200
Subject: [PATCH] notation.v: markup titles in coqdoc

---
 theories/bi/notation.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 94a58c036..0a8a75a69 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -1,6 +1,6 @@
 (** Just reserve the notation. *)
 
-(** Turnstiles *)
+(** * Turnstiles *)
 Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
 Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
 Reserved Notation "(⊢)".
@@ -14,7 +14,7 @@ Reserved Notation "('⊣⊢@{' PROP } )".
 Reserved Notation "⊢ Q" (at level 20, Q at level 200).
 Reserved Notation "'⊢@{' PROP } Q" (at level 20, Q at level 200).
 
-(** BI connectives *)
+(** * BI connectives *)
 Reserved Notation "'emp'".
 Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
 Reserved Notation "P ∗ Q" (at level 80, right associativity).
@@ -58,7 +58,7 @@ Reserved Notation "â– ? p P" (at level 20, p at level 9, P at level 20,
 Reserved Notation "'<obj>' P" (at level 20, right associativity).
 Reserved Notation "'<subj>' P" (at level 20, right associativity).
 
-(** Update modalities *)
+(** * Update modalities *)
 Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==>  Q").
 Reserved Notation "P ==∗ Q"
   (at level 99, Q at level 200, format "'[' P  '/' ==∗  Q ']'").
@@ -102,7 +102,7 @@ Reserved Notation "P ={ E1 , E2 }▷=∗^ n Q"
   (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
    format "P  ={ E1 , E2 }▷=∗^ n  Q").
 
-(** Big Ops *)
+(** * Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
   (at level 200, l at level 10, k, x at level 1, right associativity,
    format "[∗  list]  k ↦ x  ∈  l ,  P").
-- 
GitLab