amadouage de coqweb

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

3 files changed, 40 insertions, 33 deletions

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 69ce3b6f89..4f9e43be50 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require ZArith.
 Require Omega.
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index 45ad93aba0..6f68d7ad9c 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -6,19 +6,19 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (****************************************************************************)
 (*  The integer logarithms with base 2. There are three logarithms,	    *)
 (*    depending on the rounding of the real 2-based logarithm : 	    *)
 (*									    *)
-(*  Log_inf : y = (Log_inf x) iff 2^y <= x < 2^(y+1)			    *)
-(*  Log_sup : y = (Log_sup x) iff 2^(y-1) < x <= 2^y			    *)
-(*  Log_nearest : y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)	    *)
+(*  [Log_inf : y = (Log_inf x) iff 2^y <= x < 2^(y+1)]			    *)
+(*  [Log_sup : y = (Log_sup x) iff 2^(y-1) < x <= 2^y]			    *)
+(*  [Log_nearest : y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)]	    *)
 (*									    *)
-(*  (Log_inf x) is the biggest integer that is smaller than (Log x)	    *)
-(*  (Log_inf x) is the smallest integer that is bigger than (Log x)	    *)
-(*  (Log_nearest x) is the integer nearest from (Log x). 		    *)
+(*  [Log_inf x] is the biggest integer that is smaller than [Log x]	    *)
+(*  [Log_inf x] is the smallest integer that is bigger than [Log x]	    *)
+(*  [Log_nearest x] is the integer nearest from [Log x]. 		    *)
 (****************************************************************************)
 
 Require ZArith.
@@ -28,7 +28,7 @@ Require Zpower.
 
 Section Log_pos. (* Log of positive integers *)
 
-(* First we build log_inf and log_sup *)
+(* First we build [log_inf] and [log_sup] *)
 
 Fixpoint log_inf [p:positive] : Z :=  
   Cases p of
@@ -45,10 +45,10 @@ Fixpoint log_sup [p:positive] : Z :=
 
 Hints Unfold log_inf log_sup.
 
-(* Then we give the specifications of log_inf and log_sup 
+(* Then we give the specifications of [log_inf] and [log_sup] 
   and prove their validity *)
 
-(* Hints Resolve ZERO_le_S : zarith. *)
+(*i Hints Resolve ZERO_le_S : zarith. i*)
 Hints Resolve Zle_trans : zarith.
 
 Theorem log_inf_correct : (x:positive) ` 0 <= (log_inf x)` /\
@@ -83,8 +83,8 @@ Lemma log_sup_correct1 : (p:positive)` 0 <= (log_sup p)`.
 Induction p; Intros; Simpl; Auto with zarith.
 Save.
 
-(* For every p, either p is a power of two and (log_inf p)=(log_sup p)
-  either (log_sup p)=(log_inf p)+1 *)
+(* For every p, either p is a power of two and [(log_inf p)=(log_sup p)]
+  either [(log_sup p)=(log_inf p)+1] *)
 
 Theorem log_sup_log_inf : (p:positive)
   either (POS p)=(two_p (log_inf p)) 
@@ -112,7 +112,7 @@ Theorem log_sup_correct2 : (x:positive)
 
 Intro.
 Elim (log_sup_log_inf x).
-(* x is a power of two and log_sup = log_inf *)
+(* x is a power of two and [log_sup = log_inf] *)
 Intros (E1,E2); Rewrite E2.
 Split ; [ Apply two_p_pred; Apply log_sup_correct1 | Apply Zle_n ].
 Intros (E1,E2); Rewrite E2.
@@ -176,7 +176,7 @@ Case p0; Intros; Auto with zarith.
 Auto.
 Save.
 
-(*******************
+(i*******************
 Theorem log_near_correct: (p:positive)
   `| (two_p (log_near p)) - (POS p) | <= (POS p)-(two_p (log_inf p))`
   /\`| (two_p (log_near p)) - (POS p) | <= (two_p (log_sup p))-(POS p)`.
@@ -196,7 +196,7 @@ Unfold log_near; Fold log_near.
 Unfold log_inf; Fold log_inf.
 Repeat Rewrite E1.
 Split.
-***********************************)
+***********************************i)
 
 End Log_pos.
 
@@ -232,7 +232,7 @@ Induction n; Intros;
 | Rewrite -> inj_S; Rewrite <- H; Reflexivity].
 Save.
 
-(* (Is_power p) means that p is a power of two *)
+(* [Is_power p] means that p is a power of two *)
 Fixpoint Is_power[p:positive] : Prop :=
   Cases p of
     xH => True
@@ -262,3 +262,10 @@ Induction p;
 Save.
 
 End divers.
+
+
+
+
+
+
+
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 1d97275736..19ac1827b3 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require ZArith.
 Require Omega.
@@ -14,13 +14,13 @@ Require Zcomplements.
 
 Section section1.
 
-(* (Zpower_nat z n) is the n-th power of x when n is an unary
+(* [Zpower_nat z n] is the n-th power of x when n is an unary
     integer (type nat) and z an signed integer (type Z) *) 
 
 Definition Zpower_nat := 
   [z:Z][n:nat] (iter_nat n Z ([x:Z]` z * x `) `1`).
  
-(* Zpower_nat_is_exp says Zpower_nat is a morphism for
+(* [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
    plus : nat->nat and Zmult : Z->Z *)
 
 Lemma Zpower_nat_is_exp : 
@@ -33,7 +33,7 @@ Intros; Elim n;
   Apply Zmult_assoc].
 Save.
 
-(* (Zpower_nat z n) is the n-th power of x when n is an binary
+(* [Zpower_nat z n] is the n-th power of x when n is an binary
    integer (type positive) and z an signed integer (type Z) *) 
 
 Definition Zpower_pos := 
@@ -48,8 +48,8 @@ Theorem Zpower_pos_nat :
 Intros; Unfold Zpower_pos; Unfold Zpower_nat; Apply iter_convert.
 Save.
 
-(* Using the theorem Zpower_pos_nat and the lemma Zpower_nat_is_exp we
-   deduce that the function [n:positive](Zpower_pos z n) is a morphism
+(* Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
+   deduce that the function [[n:positive](Zpower_pos z n)] is a morphism
    for add : positive->positive and Zmult : Z->Z *)
 
 Theorem Zpower_pos_is_exp : 
@@ -96,10 +96,10 @@ Section Powers_of_2.
 
 (* For the powers of two, that will be widely used, a more direct
    calculus is possible. We will also prove some properties such
-   as (x:positive) x < 2^x that are true for all integers bigger
+   as [(x:positive) x < 2^x] that are true for all integers bigger
    than 2 but more difficult to prove and useless. *)     
 
-(* shift n m computes 2^n * m, or m shifted by n positions *)
+(* [shift n m] computes [2^n * m], or m shifted by n positions *)
 
 Definition shift_nat := 
   [n:nat][z:positive](iter_nat n positive xO z). 
@@ -148,7 +148,7 @@ Rewrite -> (shift_nat_correct n).
 Omega.
 Save.
   
-(* Second we show that two_power_pos and two_power_nat are the same *)
+(* Second we show that [two_power_pos] and [two_power_nat] are the same *)
 Lemma shift_pos_nat : (p:positive)(x:positive)
   (shift_pos p x)=(shift_nat (convert p) x).
 
@@ -165,7 +165,7 @@ Apply f_equal with f:=POS.
 Apply shift_pos_nat.
 Save.
 
-(* Then we deduce that two_power_pos is also correct *)
+(* Then we deduce that [two_power_pos] is also correct *)
 
 Theorem shift_pos_correct :
   (p,x:positive) ` (POS (shift_pos p x)) = (Zpower_pos 2 p) * (POS x)`.
@@ -197,10 +197,10 @@ Rewrite -> (two_power_pos_correct y).
 Apply Zpower_pos_is_exp.
 Save.
 
-(* The exponentiation z -> 2^z for z a signed integer.   *)
-(* For convenience, we assume that 2^z = 0 for all z <0 *)
-(* We could also define a inductive type Log_result with *)
-(* 3 contructors Zero | Pos positive -> | minus_infty    *)
+(* The exponentiation [z -> 2^z] for z a signed integer.   *)
+(* For convenience, we assume that [2^z = 0] for all [z <0] *)
+(* We could also define a inductive type [Log_result] with *)
+(* 3 contructors [ Zero | Pos positive -> | minus_infty]    *)
 (* but it's more complexe and not so useful.		 *)
  
 Definition two_p :=
@@ -282,9 +282,9 @@ Section power_div_with_rest.
 
 (* Division by a power of two
   To n:Z and p:positive q,r are associated such that
-    n = 2^p.q + r and 0 <= r < 2^p *)
+    [n = 2^p.q + r] and [0 <= r < 2^p] *)
 
-(* Invariant : d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d' *)
+(* Invariant : [d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'] *)
 Definition Zdiv_rest_aux :=
   [qrd:(Z*Z)*Z] 
   let (qr,d)=qrd in let (q,r)=qr in