From 67f72c93f5f364591224a86c52727867e02a8f71 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 14 Feb 2002 14:39:07 +0000
Subject: option -dump-glob pour coqdoc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Raxioms.v | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

(limited to 'theories/Reals/Raxioms.v')

diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index f1aa04519..1c7674f4e 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 (*********************************************************)
-(*s    {Axiomatisation of the classical reals}           *)
+(**    Axiomatisation of the classical reals             *)
 (*********************************************************)
 
 Require Export ZArith.
@@ -17,10 +17,11 @@ Require Export Rsyntax.
 Require Export TypeSyntax.
 
 (*********************************************************)
-(*              {Field axioms}                           *)
+(*               Field axioms                            *)
 (*********************************************************)
+
 (*********************************************************)
-(*s      Addition                                        *)
+(**      Addition                                        *)
 (*********************************************************)
 
 (**********)
@@ -40,7 +41,7 @@ Axiom Rplus_Ol:(r:R)``0+r==r``.
 Hints Resolve Rplus_Ol : real.
 
 (***********************************************************)       
-(*s       Multiplication                                   *)
+(**       Multiplication                                   *)
 (***********************************************************)
 
 (**********)
@@ -64,7 +65,7 @@ Axiom R1_neq_R0:``1<>0``.
 Hints Resolve R1_neq_R0 : real.
 
 (*********************************************************)
-(*s      Distributivity                                  *)
+(**      Distributivity                                  *)
 (*********************************************************)
 
 (**********)
@@ -72,17 +73,17 @@ Axiom Rmult_Rplus_distr:(r1,r2,r3:R)``r1*(r2+r3)==(r1*r2)+(r1*r3)``.
 Hints Resolve Rmult_Rplus_distr : real v62.
 
 (*********************************************************)
-(*       Order axioms                                    *)
+(**      Order axioms                                    *)
 (*********************************************************)
 (*********************************************************)
-(*s      Total Order                                     *)
+(**      Total Order                                     *)
 (*********************************************************)
 
 (**********)
 Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT ``r1<r2`` r1==r2) ``r1>r2``).
 
 (*********************************************************)
-(*s      Lower                                           *)
+(**      Lower                                           *)
 (*********************************************************)
 
 (**********)
@@ -101,7 +102,7 @@ Axiom Rlt_monotony:(r,r1,r2:R)``0<r``->``r1<r2``->``r*r1<r*r2``.
 Hints Resolve Rlt_antisym Rlt_compatibility Rlt_monotony : real.
 
 (**********************************************************) 
-(*s      Injection from N to R                            *)
+(**      Injection from N to R                            *)
 (**********************************************************)
 
 (**********)
@@ -112,7 +113,7 @@ Fixpoint INR [n:nat]:R:=(Cases n of
                         end).  
 
 (**********************************************************) 
-(*s      Injection from Z to R                            *)
+(**      Injection from [Z] to [R]                        *)
 (**********************************************************)
 
 (**********)
@@ -123,14 +124,14 @@ Definition IZR:Z->R:=[z:Z](Cases z of
                            end).  
 
 (**********************************************************)
-(*s      R Archimedian                                    *)
+(**      [R] Archimedian                                  *)
 (**********************************************************)
 
 (**********)
 Axiom archimed:(r:R)``(IZR (up r)) > r``/\``(IZR (up r))-r <= 1``.
 
 (**********************************************************)
-(*s      R Complete                                        *)
+(**      [R] Complete                                     *)
 (**********************************************************)
 
 (**********)
-- 
cgit v1.2.3