transcript: improved debuugging facilities

[helm.git] / helm / software / matita / contribs / procedural / Coq / ZArith / Zbinary.mma

diff --git a/helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma b/helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma
index a1c27a484a80a791c293f73a0a1dabf37f2d8526..87df305f6bbae4efa094f7e4c1edcc6d72abd329 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma
+++ b/helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma
@@ -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.
 *)