Du bon usage des commentaires coqweb

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

1 files changed, 16 insertions, 12 deletions

diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v
index 57aef2a5f..d54d1a0a2 100644
--- a/theories/ZArith/Zhints.v
+++ b/theories/ZArith/Zhints.v
@@ -11,6 +11,8 @@
 (* This file centralizes the lemmas about Z, classifying them *)
 (* according to the way they can be used in automatic search  *)
 
+(*i*)
+
 (* Lemmas which clearly leads to simplification during proof search are *)
 (* declared as Hints. A definite status (Hint or not) for the other lemmas *)
 (* remains to be given *)
@@ -36,8 +38,8 @@ Require Wf_Z.
 (* No subgoal or smaller subgoals                                     *)
 
 Hints Resolve
-  (* A) Reversible simplification lemmas (no loss of information)       *)
-  (* Should clearly declared as hints                                   *)
+  (* A) Reversible simplification lemmas (no loss of information)      *)
+  (* Should clearly declared as hints                                  *)
   
   (* Lemmas ending by eq *)
   Zeq_S (* :(n,m:Z)`n = m`->`(Zs n) = (Zs m)` *)
@@ -99,7 +101,7 @@ Hints Resolve
 (*         Reversible lemmas relating operators                       *)
 (* Probably to be declared as hints but need to define precedences    *)
 
-(*i A) Conversion between comparisons/predicates and arithmetic operators
+(* A) Conversion between comparisons/predicates and arithmetic operators
 
 (* Lemmas ending by eq *)
 Zegal_left: (x,y:Z)`x = y`->`x+(-y) = 0`
@@ -186,12 +188,12 @@ Zgt_pred: (n,p:Z)`p > (Zs n)`->`(Zpred p) > n`
 (* Lemmas ending by Zlt *)
 Zlt_pred: (n,p:Z)`(Zs n) < p`->`n < (Zpred p)`
 
-i*)
+*)
 
 (**********************************************************************)
 (*                 Useful Bottom-up lemmas                            *)
 
-(*i A) Bottom-up simplification: should be used 
+(* A) Bottom-up simplification: should be used 
 
 (* Lemmas ending by eq *)
 Zeq_add_S: (n,m:Z)`(Zs n) = (Zs m)`->`n = m`
@@ -233,11 +235,11 @@ pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y`
 (* Lemmas ending by Zle *)
 Zmult_le: (x,y:Z)`x > 0`->`0 <= y*x`->`0 <= y`
 OMEGA1: (x,y:Z)`x = y`->`0 <= x`->`0 <= y`
-i*)
+*)
 
 (**********************************************************************)
 (*           Irreversible lemmas with meta-variables                  *)
-(*i To be used by EAuto                                                
+(* To be used by EAuto                                                
 
 Hints Immediate
 (* Lemmas ending by eq *)
@@ -259,13 +261,13 @@ Zle_lt_trans: (n,m,p:Z)`n <= m`->`m < p`->`n < p`
 
 (* Lemmas ending by Zle *)
 Zle_trans: (n,m,p:Z)`n <= m`->`m <= p`->`n <= p`
-i*)
+*)
 
 (**********************************************************************)
 (*               Unclear or too specific lemmas                       *)
 (* Not to be used ??                                                  *)
 
-(*i A) Irreversible and too specific (not enough regular) 
+(* A) Irreversible and too specific (not enough regular) 
 
 (* Lemmas ending by Zle *)
 Zle_mult: (x,y:Z)`x > 0`->`0 <= y`->`0 <= y*x`
@@ -291,11 +293,11 @@ Zmult_le_approx: (x,y,z:Z)`x > 0`->`x > z`->`0 <= y*x+z`->`0 <= y`
 
 (* Lemmas ending by Zlt *)
 Zlt_minus: (n,m:Z)`0 < m`->`n-m < n`
-i*)
+*)
 
 (**********************************************************************)
 (*               Lemmas to be used as rewrite rules                   *)
-(*i but can also be used as hints                                      
+(* but can also be used as hints                                      
 
 (* Left-to-right simplification lemmas (a symbol disappears) *)
 
@@ -374,4 +376,6 @@ inj_minus2: (x,y:nat)(gt y x)->`(inject_nat (minus x y)) = 0`
 
 (* Too specific ? *)
 Zred_factor5: (x,y:Z)`x*0+y = y`
-i*)
+*)
+
+(*i*)