diff options
| author | herbelin | 2006-03-04 19:18:34 +0000 |
|---|---|---|
| committer | herbelin | 2006-03-04 19:18:34 +0000 |
| commit | ff949bd2a1f4ca4e1428e2ed96c9e46cc0d14cca (patch) | |
| tree | 4571ae0e6ce19d1bf38210ce34572ef58e113022 | |
| parent | fe3181f913e3999eaf18eaad39a053ee89b76b86 (diff) | |
Titres moins envahissants pour coqdoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8121 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rwxr-xr-x | theories/Init/Logic.v | 6 |
1 files 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]. |