From ff949bd2a1f4ca4e1428e2ed96c9e46cc0d14cca Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 4 Mar 2006 19:18:34 +0000
Subject: Titres moins envahissants pour coqdoc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8121 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Logic.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 8a11a43bad..4907c93a40 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -12,7 +12,7 @@ Set Implicit Arguments.
 
 Require Import Notations.
 
-(** * Propositional connectives *)
+(** *** Propositional connectives *)
 
 (** [True] is the always true proposition *)
 Inductive True : Prop :=
@@ -97,7 +97,7 @@ Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
 Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
   (at level 200, right associativity) : type_scope.
 
-(** * First-order quantifiers *)
+(** *** First-order quantifiers *)
 
 (** [ex P], or simply [exists x, P x], or also [exists x:A, P x],
     expresses the existence of an [x] of some type [A] in [Set] which
@@ -160,7 +160,7 @@ Section universal_quantification.
 
 End universal_quantification.
 
-(** * Equality *)
+(** *** Equality *)
 
 (** [eq x y], or simply [x=y] expresses the equality of [x] and
     [y]. Both [x] and [y] must belong to the same type [A].
-- 
cgit v1.2.3