patch Bvector: args implicites

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

1 files changed, 15 insertions, 15 deletions

diff --git a/theories/ZArith/Zbinary.v b/theories/ZArith/Zbinary.v
index cd8872dac..c78e0a72f 100644
--- a/theories/ZArith/Zbinary.v
+++ b/theories/ZArith/Zbinary.v
@@ -17,10 +17,10 @@ Require Export Zpower.
 Require Import Omega.
 
 (*
-L'évaluation des vecteurs de booléens se font à la fois en binaire et
-en complément à deux. Le nombre appartient à Z. 
+L'évaluation des vecteurs de booléens se font à la fois en binaire et
+en complément à deux. Le nombre appartient à Z. 
 On utilise donc Omega pour faire les calculs dans Z.
-De plus, on utilise les fonctions 2^n où n est un naturel, ici la longueur.
+De plus, on utilise les fonctions 2^n où n est un naturel, ici la longueur.
 	two_power_nat = [n:nat](POS (shift_nat n xH))
      		: nat->Z
 	two_power_nat_S
@@ -33,12 +33,12 @@ De plus, on utilise les fonctions 2^n où n est un naturel, ici la longueur.
 Section VALUE_OF_BOOLEAN_VECTORS.
 
 (*
-Les calculs sont effectués dans la convention positive usuelle.
-Les valeurs correspondent soit à l'écriture binaire (nat), 
-soit au complément à deux (int).
-On effectue le calcul suivant le schéma de Horner.
-Le complément à deux n'a de sens que sur les vecteurs de taille 
-supérieure ou égale à un, le bit de signe étant évalué négativement.
+Les calculs sont effectués dans la convention positive usuelle.
+Les valeurs correspondent soit à l'écriture binaire (nat), 
+soit au complément à deux (int).
+On effectue le calcul suivant le schéma de Horner.
+Le complément à deux n'a de sens que sur les vecteurs de taille 
+supérieure ou égale à un, le bit de signe étant évalué négativement.
 *)
 
 Definition bit_value (b:bool) : Z :=
@@ -84,11 +84,11 @@ Section ENCODING_VALUE.
 
 (*
 On calcule la valeur binaire selon un schema de Horner.
-Le calcul s'arrete à la longueur du vecteur sans vérification.
+Le calcul s'arrete à la longueur du vecteur sans vérification.
 On definit une fonction Zmod2 calquee sur Zdiv2 mais donnant le quotient
 de la division z=2q+r avec 0<=r<=1.
-La valeur en complément à deux est calculée selon un schema de Horner
-avec Zmod2, le paramètre est la taille moins un.
+La valeur en complément à deux est calculée selon un schema de Horner
+avec Zmod2, le paramètre est la taille moins un.
 *)
 
 Definition Zmod2 (z:Z) :=
@@ -186,7 +186,7 @@ Meriterait d'etre reecrite.
 
 Lemma binary_value_Sn :
  forall (n:nat) (b:bool) (bv:Bvector n),
-   binary_value (S n) (Vcons bool b n bv) =
+   binary_value (S n) (Vcons b bv) =
    (bit_value b + 2 * binary_value n bv)%Z.
 Proof.
 	intros; auto.
@@ -355,8 +355,8 @@ End Z_BRIC_A_BRAC.
 Section COHERENT_VALUE.
 
 (*
-On vérifie que dans l'intervalle de définition les fonctions sont 
-réciproques l'une de l'autre.
+On vérifie que dans l'intervalle de définition les fonctions sont 
+réciproques l'une de l'autre.
 Elles utilisent les lemmes du bric-a-brac.
 *)