diff options
author | 2001-08-13 16:10:41 +0000 | |
---|---|---|
committer | 2001-08-13 16:10:41 +0000 | |
commit | 7a63d8f5df7ae27038c6c770c22ee3911781de85 (patch) | |
tree | 7b62e499eabb452b46e47e85c596597b590777c6 /theories | |
parent | 1e3ebfcda7a923d1c6f39eb64020f805deafba50 (diff) |
Protection des commentaires pour coqtex et coqweb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1897 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Logic/Berardi.v | 4 | ||||
-rw-r--r-- | theories/ZArith/Zhints.v | 21 |
2 files changed, 13 insertions, 12 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index ca62faca6..3ddc2fc5e 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(* This file formalizes Berardi's paradox which says that in +(*i This file formalizes Berardi's paradox which says that in the calculus of constructions, excluded middle (EM) and axiom of choice (AC) implie proof irrelevenace (PI). Here, the axiom of choice is not necessary because of the use @@ -25,7 +25,7 @@ pages = {519-525} } - *) + i*) Require Elimdep. diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v index 6c8cc88fc..57aef2a5f 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.v @@ -99,7 +99,7 @@ Hints Resolve (* Reversible lemmas relating operators *) (* Probably to be declared as hints but need to define precedences *) -(* A) Conversion between comparisons/predicates and arithmetic operators +(*i A) Conversion between comparisons/predicates and arithmetic operators (* Lemmas ending by eq *) Zegal_left: (x,y:Z)`x = y`->`x+(-y) = 0` @@ -185,12 +185,13 @@ 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 *) -(* A) Bottom-up simplification: should be used +(*i A) Bottom-up simplification: should be used (* Lemmas ending by eq *) Zeq_add_S: (n,m:Z)`(Zs n) = (Zs m)`->`n = m` @@ -232,11 +233,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 *) -(* To be used by EAuto +(*i To be used by EAuto Hints Immediate (* Lemmas ending by eq *) @@ -258,13 +259,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 ?? *) -(* A) Irreversible and too specific (not enough regular) +(*i A) Irreversible and too specific (not enough regular) (* Lemmas ending by Zle *) Zle_mult: (x,y:Z)`x > 0`->`0 <= y`->`0 <= y*x` @@ -290,11 +291,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 *) -(* but can also be used as hints +(*i but can also be used as hints (* Left-to-right simplification lemmas (a symbol disappears) *) @@ -373,4 +374,4 @@ 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*) |