option -dump-glob pour coqdoc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7

18 files changed, 112 insertions, 52 deletions

diff --git a/theories/Num/AddProps.v b/theories/Num/AddProps.v
index f30b616162..739ead5e0c 100644
--- a/theories/Num/AddProps.v
+++ b/theories/Num/AddProps.v
@@ -9,9 +9,9 @@
 Require Export Axioms.
 Require Export EqAxioms.
 
-(*s This file contains basic properties of addition with respect to equality *)
+(** This file contains basic properties of addition with respect to equality *)
 
-(*s Properties of Addition *)
+(** Properties of Addition *)
 Lemma add_x_0 : (x:N)(x+zero)=x.
 EAuto 3 with num.
 Save.
diff --git a/theories/Num/Axioms.v b/theories/Num/Axioms.v
index a8c43b6a28..e6def17761 100644
--- a/theories/Num/Axioms.v
+++ b/theories/Num/Axioms.v
@@ -5,32 +5,33 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
-(*i $Id: i*)
 
-(*s Axioms for the basic numerical operations *)
+(*i $Id$ i*)
+
+(** Axioms for the basic numerical operations *)
 Require Export Params.
 Require Export EqParams.
 Require Export NSyntax.
 
-(*s Axioms for [eq] *)
+(** Axioms for [eq] *)
 
 Axiom eq_refl : (x:N)(x=x).
 Axiom eq_sym : (x,y:N)(x=y)->(y=x).
 Axiom eq_trans : (x,y,z:N)(x=y)->(y=z)->(x=z).
 
-(*s Axioms for [add] *)
+(** Axioms for [add] *)
 
 Axiom add_sym : (x,y:N)(x+y)=(y+x).
 Axiom add_assoc_l : (x,y,z:N)((x+y)+z)=(x+(y+z)).
 Axiom add_0_x : (x:N)(zero+x)=x.
 
-(*s Axioms for [S] *)
+(** Axioms for [S] *)
 Axiom add_Sx_y : (x,y:N)((S x)+y)=(S (x+y)).
 
-(*s Axioms for [one] *)
+(** Axioms for [one] *)
 Axiom S_0_1 : (S zero)=one.
 
-(*s Axioms for [<], 
+(** Axioms for [<], 
     properties of [>], [<=] and [>=] will be derived from [<] *)
 
 Axiom lt_trans : (x,y,z:N)x<y->y<z->x<z.
diff --git a/theories/Num/Definitions.v b/theories/Num/Definitions.v
index 2b908f5cda..7a20b37ba3 100644
--- a/theories/Num/Definitions.v
+++ b/theories/Num/Definitions.v
@@ -5,10 +5,11 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
-(*i $Id $ i*)
 
-(*s 
-  Axiomatisation of a numerical set 
+(*i $Id$ i*)
+
+(** Axiomatisation of a numerical set 
+
   It will be instantiated by Z and R later on
   We choose to introduce many operation to allow flexibility in definition 
   ([S] is primitive in the definition of [nat] while [add] and [one] 
@@ -21,7 +22,7 @@ Parameter one:N.
 Parameter add:N->N->N.
 Parameter S:N->N.
 
-(*s Relations *)
+(** Relations *)
 Parameter eq,lt,le,gt,ge:N->N->Prop.    
 Definition neq [x,y:N] := (eq x y)->False.
 
diff --git a/theories/Num/DiscrAxioms.v b/theories/Num/DiscrAxioms.v
index 83b2e42f47..fae4b6d96d 100644
--- a/theories/Num/DiscrAxioms.v
+++ b/theories/Num/DiscrAxioms.v
@@ -5,12 +5,13 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
+
 (*i $Id$ i*)
 
 Require Export Params.
 Require Export NSyntax.
 
-(*s Axiom for a discrete set *)
+(** Axiom for a discrete set *)
 
 Axiom lt_x_Sy_le : (x,y:N)(x<(S y))->(x<=y).
 Hints Resolve lt_x_Sy_le : num.
diff --git a/theories/Num/DiscrProps.v b/theories/Num/DiscrProps.v
index 5554357e8c..fd578ad17a 100644
--- a/theories/Num/DiscrProps.v
+++ b/theories/Num/DiscrProps.v
@@ -5,12 +5,13 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
+
 (*i $Id$ i*)
 
 Require Export DiscrAxioms.
 Require Export LtProps.
 
-(*s Properties of a discrete order *)
+(** Properties of a discrete order *)
 
 Lemma lt_le_Sx_y : (x,y:N)(x<y) -> ((S x)<=y).
 EAuto with num.
diff --git a/theories/Num/EqAxioms.v b/theories/Num/EqAxioms.v
index 957a8edf03..4e2f362393 100644
--- a/theories/Num/EqAxioms.v
+++ b/theories/Num/EqAxioms.v
@@ -1,23 +1,31 @@
-(*i $Id: i*)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
-(*s Axioms for equality *)
+(*i $Id$ i*)
+
+(** Axioms for equality *)
 Require Export Params.
 Require Export EqParams.
 Require Export NSyntax.
 
-(*s Basic Axioms for [eq] *)
+(** Basic Axioms for [eq] *)
 
 Axiom eq_refl : (x:N)(x=x).
 Axiom eq_sym : (x,y:N)(x=y)->(y=x).
 Axiom eq_trans : (x,y,z:N)(x=y)->(y=z)->(x=z).
 
-(*s Axioms for [eq] and [add] *)
+(** Axioms for [eq] and [add] *)
 Axiom add_eq_compat : (x1,x2,y1,y2:N)(x1=x2)->(y1=y2)->(x1+y1)=(x2+y2).
 
-(*s Axioms for [eq] and [S] *)
+(** Axioms for [eq] and [S] *)
 Axiom S_eq_compat : (x,y:N)(x=y)->(S x)=(S y).
 
-(*s Axioms for [eq] and [<] *)
+(** Axioms for [eq] and [<] *)
 Axiom lt_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<x2)->(y1<y2).
 
 Hints Resolve eq_refl eq_trans add_eq_compat S_eq_compat lt_eq_compat : num.
diff --git a/theories/Num/EqParams.v b/theories/Num/EqParams.v
index 3f15696737..f7fec9f92f 100644
--- a/theories/Num/EqParams.v
+++ b/theories/Num/EqParams.v
@@ -1,6 +1,14 @@
-(*i $Id $ i*)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
-(*s Equality is introduced as an independant parameter, it could be 
+(*i $Id$ i*)
+
+(** Equality is introduced as an independant parameter, it could be 
     instantiated with Leibniz equality *)
 Require Export Params.
 
diff --git a/theories/Num/GeAxioms.v b/theories/Num/GeAxioms.v
index f242479758..87e6663265 100644
--- a/theories/Num/GeAxioms.v
+++ b/theories/Num/GeAxioms.v
@@ -5,11 +5,13 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
-(*i $Id: i*)
+
+(*i $Id$ i*)
+
 Require Export Axioms.
 Require Export LtProps.
 
-(*s Axiomatizing [>=] from [<] *)
+(** Axiomatizing [>=] from [<] *)
 
 Axiom not_lt_ge : (x,y:N)~(x<y)->(x>=y).
 Axiom ge_not_lt : (x,y:N)(x>=y)->~(x<y).
diff --git a/theories/Num/GtAxioms.v b/theories/Num/GtAxioms.v
index 548d43cdf0..f4dc010902 100644
--- a/theories/Num/GtAxioms.v
+++ b/theories/Num/GtAxioms.v
@@ -5,12 +5,13 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
-(*i $Id: i*)
+
+(*i $Id$ i*)
+
 Require Export Axioms.
 Require Export LeProps.
 
-(*s Axiomatizing [>] from [<] *)
-
+(** Axiomatizing [>] from [<] *)
 
 Axiom not_le_gt : (x,y:N)~(x<=y)->(x>y).
 Axiom gt_not_le : (x,y:N)(x>y)->~(x<=y).
diff --git a/theories/Num/LeAxioms.v b/theories/Num/LeAxioms.v
index 668c4677de..e1a7710fee 100644
--- a/theories/Num/LeAxioms.v
+++ b/theories/Num/LeAxioms.v
@@ -5,11 +5,13 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
-(*i $Id: i*)
+
+(*i $Id$ i*)
+
 Require Export Axioms.
 Require Export LtProps.
 
-(*s Axiomatizing [<=] from [<] *)
+(** Axiomatizing [<=] from [<] *)
 
 Axiom lt_or_eq_le : (x,y:N)((x<y)\/(x=y))->(x<=y).
 Axiom le_lt_or_eq : (x,y:N)(x<=y)->(x<y)\/(x=y).
diff --git a/theories/Num/LeProps.v b/theories/Num/LeProps.v
index c476bb2066..bf7af0d667 100644
--- a/theories/Num/LeProps.v
+++ b/theories/Num/LeProps.v
@@ -5,10 +5,11 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
+
 Require Export LtProps.
 Require Export LeAxioms.
 
-(*s Properties of the relation [<=] *)
+(** Properties of the relation [<=] *)
 
 Lemma lt_le : (x,y:N)(x<y)->(x<=y).
 Auto with num.
@@ -18,7 +19,7 @@ Lemma eq_le : (x,y:N)(x=y)->(x<=y).
 Auto with num.
 Save.
 
-(*s compatibility with equality *)
+(** compatibility with equality *)
 Lemma le_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<=x2)->(y1<=y2).
 Intros x1 x2 y1 y2 eq1 eq2 le1; Case le_lt_or_eq with 1:=le1; Intro.
 EAuto with num.
@@ -26,7 +27,7 @@ Apply eq_le; Apply eq_trans with x1; EAuto with num.
 Save.
 Hints Resolve le_eq_compat : num.
 
-(*s Transitivity *)
+(** Transitivity *)
 Lemma le_trans : (x,y,z:N)(x<=y)->(y<=z)->(x<=z).
 Intros x y z le1 le2.
 Case le_lt_or_eq with 1:=le1; Intro.
@@ -35,7 +36,7 @@ EAuto with num.
 Save.
 Hints Resolve le_trans : num.
 
-(*s compatibility with equality, addition and successor *)
+(** compatibility with equality, addition and successor *)
 Lemma le_add_compat_l : (x,y,z:N)(x<=y)->((x+z)<=(y+z)).
 Intros x y z le1.
 Case le_lt_or_eq with 1:=le1; EAuto with num.
@@ -60,7 +61,7 @@ Save.
 Hints Resolve le_S_compat : num.
 
 
-(*s relating [<=] with [<] *)
+(** relating [<=] with [<] *)
 Lemma le_lt_x_Sy : (x,y:N)(x<=y)->(x<(S y)).
 Intros x y le1.
 Case le_lt_or_eq with 1:=le1; Auto with num.
@@ -78,7 +79,7 @@ Case le_lt_or_eq with 1:=le1; EAuto with num.
 Save.
 Hints Immediate le_Sx_y_lt : num.
 
-(*s Combined transitivity *)
+(** Combined transitivity *)
 Lemma lt_le_trans : (x,y,z:N)(x<y)->(y<=z)->(x<z).
 Intros x y z lt1 le1; Case le_lt_or_eq with 1:= le1; EAuto with num.
 Save.
@@ -88,7 +89,7 @@ Intros x y z le1 lt1; Case le_lt_or_eq with 1:= le1; EAuto with num.
 Save.
 Hints Immediate lt_le_trans le_lt_trans : num.
 
-(*s weaker compatibility results involving [<] and [<=] *)
+(** weaker compatibility results involving [<] and [<=] *)
 Lemma lt_add_compat_weak_l : (x1,x2,y1,y2:N)(x1<=x2)->(y1<y2)->((x1+y1)<(x2+y2)).
 Intros; Apply lt_le_trans with (x1+y2); Auto with num.
 Save.
diff --git a/theories/Num/LtProps.v b/theories/Num/LtProps.v
index ef9e523108..9b77b38939 100644
--- a/theories/Num/LtProps.v
+++ b/theories/Num/LtProps.v
@@ -5,11 +5,12 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
+
 Require Export Axioms.
 Require Export AddProps.
 Require Export NeqProps.
 
-(*s This file contains basic properties of the less than relation *)
+(** This file contains basic properties of the less than relation *)
 
 
 Lemma lt_anti_sym : (x,y:N)x<y->~(y<x).
@@ -43,7 +44,7 @@ EAuto with num.
 Save.
 Hints Immediate lt_Sx_y_lt : num.
 
-(*s Relating [<] and [=] *)
+(** Relating [<] and [=] *)
 
 Lemma lt_neq : (x,y:N)(x<y)->(x<>y).
 Red; Intros x y lt1 eq1; Apply (lt_anti_refl x); EAuto with num.
@@ -55,7 +56,7 @@ Intros x y lt1 ; Apply neq_sym; Auto with num.
 Save.
 Hints Immediate lt_neq_sym : num.
 
-(*s Application to inequalities properties *)
+(** Application to inequalities properties *)
 
 Lemma neq_x_Sx : (x:N)x<>(S x).
 Auto with num.
@@ -67,7 +68,7 @@ Auto with num.
 Save.
 Hints Resolve neq_0_1 : num.
 
-(*s Relating [<] and [+] *)
+(** Relating [<] and [+] *)
 
 Lemma lt_add_compat_r : (x,y,z:N)(x<y)->((z+x)<(z+y)).
 Intros x y z H; Apply lt_eq_compat with (x+z) (y+z); Auto with num.
diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v
index 364fb944a0..7787c1f039 100644
--- a/theories/Num/NSyntax.v
+++ b/theories/Num/NSyntax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*s Syntax for arithmetic *)
+(** Syntax for arithmetic *)
 
 Require Export Params.
 
diff --git a/theories/Num/NeqAxioms.v b/theories/Num/NeqAxioms.v
index 303d30cf04..85bd166565 100644
--- a/theories/Num/NeqAxioms.v
+++ b/theories/Num/NeqAxioms.v
@@ -1,6 +1,14 @@
-(*i $Id $ i*)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
-(*s InEquality is introduced as an independant parameter, it could be 
+(*i $Id$ i*)
+
+(** InEquality is introduced as an independant parameter, it could be 
     instantiated with the negation of equality *)
 
 Require Export EqParams.
diff --git a/theories/Num/NeqDef.v b/theories/Num/NeqDef.v
index a9ad0dd0b0..c13f262472 100644
--- a/theories/Num/NeqDef.v
+++ b/theories/Num/NeqDef.v
@@ -1,6 +1,14 @@
-(*i $Id $ i*)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
-(*s DisEquality is defined as the negation of equality *)
+(*i $Id$ i*)
+
+(** DisEquality is defined as the negation of equality *)
 
 Require Params.
 Require EqParams.
diff --git a/theories/Num/NeqParams.v b/theories/Num/NeqParams.v
index 0486eb24ad..4e651954f2 100644
--- a/theories/Num/NeqParams.v
+++ b/theories/Num/NeqParams.v
@@ -1,6 +1,14 @@
-(*i $Id $ i*)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
-(*s InEquality is introduced as an independant parameter, it could be 
+(*i $Id$ i*)
+
+(** InEquality is introduced as an independant parameter, it could be 
     instantiated with the negation of equality *)
 
 Require Export Params.
diff --git a/theories/Num/NeqProps.v b/theories/Num/NeqProps.v
index ca521493dd..6109c1f801 100644
--- a/theories/Num/NeqProps.v
+++ b/theories/Num/NeqProps.v
@@ -12,7 +12,7 @@ Require Export EqParams.
 Require Export EqAxioms.
 
 
-(*s This file contains basic properties of disequality *)
+(** This file contains basic properties of disequality *)
 
 Lemma neq_antirefl : (x:N)~(x<>x).
 Auto with num.
diff --git a/theories/Num/Params.v b/theories/Num/Params.v
index a7be171b8d..91c1320957 100644
--- a/theories/Num/Params.v
+++ b/theories/Num/Params.v
@@ -1,7 +1,16 @@
-(*i $Id $ i*)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
-(*s 
+(*i $Id$ i*)
+
+(** 
   Axiomatisation of a numerical set 
+
   It will be instantiated by Z and R later on
   We choose to introduce many operation to allow flexibility in definition 
   ([S] is primitive in the definition of [nat] while [add] and [one] 
@@ -14,7 +23,7 @@ Parameter one:N.
 Parameter add:N->N->N.
 Parameter S:N->N.
 
-(*s Relations, equality is defined separately *)
+(** Relations, equality is defined separately *)
 Parameter lt,le,gt,ge:N->N->Prop.