X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2FCoq%2FZArith%2FZbinary.mma;h=1950bdc0665f8e78f010bfc6150630e43717a992;hb=3e758134d629980e9bf018a913404b98eccc514c;hp=a1c27a484a80a791c293f73a0a1dabf37f2d8526;hpb=29714797b01e0ac8c22e4df2827b1785a759f482;p=helm.git

diff --git a/helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma b/helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma
index a1c27a484..1950bdc06 100644
--- a/helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma
+++ b/helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma
@@ -16,21 +16,21 @@
 
 include "Coq.ma".
 
-(*#**********************************************************************)
+(*#***********************************************************************)
 
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
-(*   \VV/  *************************************************************)
+(*   \VV/  **************************************************************)
 
-(*    //   *      This file is distributed under the terms of the      *)
+(*    //   *      This file is distributed under the terms of the       *)
 
-(*         *       GNU Lesser General Public License Version 2.1       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
 
-(*#**********************************************************************)
+(*#***********************************************************************)
 
-(*i $Id: Zbinary.v,v 1.6 2004/02/10 15:38:01 marche Exp $ i*)
+(*i $Id: Zbinary.v,v 1.6.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
 
 (*#* Bit vectors interpreted as integers. 
     Contribution by Jean Duprat (ENS Lyon). *)
@@ -42,10 +42,10 @@ include "ZArith/ZArith.ma".
 include "ZArith/Zpower.ma".
 
 (*
-L'évaluation des vecteurs de booléens se font à la fois en binaire et
-en complément à deux. Le nombre appartient à Z. 
+L'\195\\169\valuation des vecteurs de bool\195\\169\ens se font \195\\160\ la fois en binaire et
+en compl\195\\169\ment \195\\160\ deux. Le nombre appartient \195\\160\ 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\195\\185\ n est un naturel, ici la longueur.
 	two_power_nat = [n:nat](POS (shift_nat n xH))
      		: nat->Z
 	two_power_nat_S
@@ -59,12 +59,12 @@ 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\195\\169\s dans la convention positive usuelle.
+Les valeurs correspondent soit \195\\160\ l'\195\\169\criture binaire (nat), 
+soit au compl\195\\169\ment \195\\160\ deux (int).
+On effectue le calcul suivant le sch\195\\169\ma de Horner.
+Le compl\195\\169\ment \195\\160\ deux n'a de sens que sur les vecteurs de taille 
+sup\195\\169\rieure ou \195\\169\gale \195\\160\ un, le bit de signe \195\\169\tant \195\\169\valu\195\\169\ n\195\\169\gativement.
 *)
 
 inline procedural "cic:/Coq/ZArith/Zbinary/bit_value.con" as definition.
@@ -95,11 +95,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 \195\\160\ la longueur du vecteur sans v\195\\169\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\195\\169\ment \195\\160\ deux est calcul\195\\169\e selon un schema de Horner
+avec Zmod2, le param\195\\168\tre est la taille moins un.
 *)
 
 inline procedural "cic:/Coq/ZArith/Zbinary/Zmod2.con" as definition.
@@ -215,8 +215,8 @@ 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\195\\169\rifie que dans l'intervalle de d\195\\169\finition les fonctions sont 
+r\195\\169\ciproques l'une de l'autre.
 Elles utilisent les lemmes du bric-a-brac.
 *)