Ajout de shell.html.

This commit is contained in:
george 2002-11-23 15:58:15 +00:00
parent 65bf3dd129
commit 1b3f473ea8
2 changed files with 740 additions and 1 deletions

1
00TODO
View file

@ -90,7 +90,6 @@ cours/unix/imprimer.html
cours/unix/index.html cours/unix/index.html
cours/unix/jeux.html cours/unix/jeux.html
cours/unix/processus.html cours/unix/processus.html
cours/unix/shell.html
exos/contact.html exos/contact.html
exos/contact_sol.html exos/contact_sol.html
exos/cp_mv.html exos/cp_mv.html

740
unix/shell.tml Normal file
View file

@ -0,0 +1,740 @@
<?xml version="1.0" encoding="ISO-8859-1"?>
<!DOCTYPE html
PUBLIC "-//ENS/Tuteurs//DTD TML 1//EN"
"tuteurs://DTD/tml.dtd">
<html>
<head>
<title>Shell</title>
</head>
<body>
<h1>Le shell</h1>
<h2><a name="presentation">Présentation</a></h2>
<p>
Le machin qui interprète les commandes.
</p>
<h3><a name="path">Comment le shell trouve-t-il les commandes ?</a>
</h3>
<p>
La <a href="#variable">variable</a> <code>PATH</code> contient le chemin d'accès
aux commandes. Le shell l'utilise pour trouver les commandes. Il s'agit d'une
liste de répertoires séparés par des <code>:</code>. La plupart des commandes
sont en fait des programmes, c'est-à-dire des fichiers qu'on trouve dans le
système de fichiers.
</p>
<p>
Par exemple, quand vous tapez <code>ls</code>, le shell exécute le fichier
<code>/bin/ls</code>. Pour trouver ce fichier, il cherche dans le premier
répertoire du <code>PATH</code> un fichier qui s'appelle <code>ls</code>.
S'il ne trouve pas, il cherche ensuite dans le deuxième répertoire et ainsi
de suite.
</p>
<p>
S'il ne trouve la commande dans aucun répertoire du <code>PATH</code>, le shell
affiche un message d'erreur. Exemple:
</p>
<pre>
<span class="prompt">chaland ~ $</span> sl
sl: Command not found</pre>
<h3><a name="builtins">Commandes internes</a></h3>
<p>
Certaines commandes du shell ne sont pas des programmes mais des commandes
<em>internes</em> (<em>builtins functions</em>). Elles sont directement
reconnues et exécutées par le shell. Un exemple de commande interne est
<code>cd</code>. C'est le répertoire courant du shell qui est modifié par
<code>cd</code>, ce qui signifie que le script suivant :
</p>
<pre>
#! /bin/sh
cd $*</pre>
<p class="continue">
ne marche pas, car le shell lance un autre shell pour exécuter le script.
C'est ce sous-shell qui change son répertoire courant, et ce changement est
perdu quand le sous-shell meurt.
</p>
<h3><a name="prog">Quels programmes utilisent le langage du shell ?</a></h3>
<p>
Scripts pour automatiser ou systématiser des tâches,
opérations un peu compliquées.
</p>
<p>
sh : .profile (shell de login) ; sh lance un autre shell qui prend la relève
pour la session.
.xinitrc (pour lancer X)
</p>
<p>
Il existe un script spécial, qui est exécuté au moment où on se connecte. Ce
script est contenu dans le fichier <code>$HOME/.profile</code>. C'est ce
fichier qui vous dit s'il y a de nouveaux messages dans forum, si vous avez
du courrier, etc.
</p>
<p>
Ce fichier est normalement mis à jour automatiquement par les scripts de la
config conscrits. Il est néanmoins possible de le modifier pour changer des
options.
</p>
<h2><a name="ligne">La ligne de commande</a></h2>
<h3><a name="raccourcis">Raccourcis pour les noms de fichiers</a></h3>
<p>
Il est parfois ennuyeux d'avoir à taper un nom complet de fichier comme
<code>nabuchodonosor</code>. Il est encore plus ennuyeux d'avoir à taper une
liste de fichier pour les donner en arguments à une commande, comme :
</p>
<pre>cc -o foo bar.c gee.c buz.c gog.c</pre>
<p>
Pour éviter ces problèmes, on peut utiliser des <em>jokers</em>
(<em>wildcards</em> en anglais).
</p>
<h4>L'étoile</h4>
<p>
Une <strong>étoile</strong> <code>*</code> dans un nom de fichier est
interprétée par le shell comme « n'importe quelle séquence de
caractères » (mais ça ignore les fichiers dont le nom commence par un
point). Exemple:
</p>
<pre>cc -o foo *.c</pre>
<p>
Pour interpréter l'étoile, le shell va faire la liste de tous les noms de
fichiers du répertoire courant qui ne commencent pas par <code>.</code> et
qui finissent par <code>.c</code>. Ensuite, il remplace <code>*.c</code>
par cette liste (triée par ordre alphabétique) dans la ligne de commande, et
exécute le résultat, c'est-à-dire par exemple :
</p>
<pre>cc -o foo bar.c buz.c foo.c gee.c gog.c</pre>
<h4>Le point d'interrogation</h4>
<p>
On a aussi le<strong>point d'interrogation</strong> <code>?</code>, qui
remplace un (et exactement un) caractère quelconque (sauf un point en début
de nom). Par exemple, <code>ls *.?</code> liste tous les dont l'extension
ne comporte qu'un caractère (<code>.c</code>, <code>.h</code>...).
</p>
<h4>Les crochets</h4>
<p>
La forme <code>[abcd]</code> remplace un caractère quelconque parmi
<code>a</code>, <code>b</code>, <code>c</code>, <code>d</code>. Enfin,
<code>[^abcd]</code> remplace un
caractère quelconque qui ne se trouve pas parmi <code>a</code>, <code>b</code>,
<code>c</code>, <code>d</code>.
</p>
<h4>Exemple</h4>
<pre>echo /users/*</pre>
<p class="continue">
affiche à peu près la même chose que
</p>
<pre>ls /users</pre>
<p class="continue">
(La commande <code>echo</code> se contente d'afficher ses arguments.)
</p>
<p>
&icone.attention; Attention :
</p>
<ul>
<li>C'est le shell qui fait le remplacement des arguments contenant un joker.
On ne peut donc pas faire <code>mv *.c *.bak</code>, car le shell va passer à
<code>mv</code> les arguments <code>foo.c bar.c foo.bak bar.bak</code>, et
<code>mv</code> ne sait pas quel fichier remplacer.
</li>
<li>Attention aux espaces. Si vous tapez <code>rm * ~</code>, le shell remplace
l'étoile par la liste des fichiers présents, et ils seront tous effacés. Si
vous tapez <code>rm *~</code>, seuls les fichiers dont le nom finit par un tilde
seront effacés.
</li>
</ul>
<p>
Interlude: comment effacer un fichier nommé <code>?*</code> ? On ne peut
pas taper <code>rm ?*</code> car le shell remplace <code>?*</code> par la
liste de tous les fichiers du répertoire courant. On peut taper <code>rm -i
*</code> qui supprime tous les fichiers, mais en demandant confirmation à
chaque fichier. On répond <code>n</code> à toutes les questions sauf
<code>rm: remove  ?*</code>.
Autre méthode: utiliser les mécanismes de quotation.
</p>
<h3><a name="quotation">Quotation</a></h3>
<p>
Avec tous ces caractères spéciaux, comment faire pour passer des arguments
bizarres à une commande ? Par exemple, comment faire afficher un point
d'interrogation suivi d'une étoile et d'un dollar par <code>echo</code> ?
Le shell fournit des mécanismes pour ce faire. Ce sont les
<em>quotations</em>.
</p>
<h4>Le backslash (<code>\</code>)</h4>
<p>
Il suffit de précéder un caractère spécial d'un backslash, et le shell
remplace ces deux caractères par le caractère spécial seul. Évidemment, le
backslash est lui-même un caractère spécial.
</p>
<p>
Exemples:
</p>
<pre>
<span class="prompt">chaland ~ $</span> echo \?\*\$
?*$
<span class="prompt">chaland ~ $</span> echo \\\?\\\*\\\$
\?\*\$</pre>
<h4>Les apostrophes ou simples quotes (<code>'</code>)</h4>
<p>
Un autre moyen est d'inclure une chaîne de caractères entre apostrophes
(simples quotes) <code>'</code>. Tout ce qui se trouve entre deux apostrophes
sera passé tel quel par le shell à la commande.
Exemple:
</p>
<pre>
<span class="prompt">chaland ~ $</span> echo '$?*'
$?*</pre>
<h4>Les guillemets doubles ou doubles quotes (<code>"</code>)</h4>
<p>
Les guillemets se comportent comme les apostrophes, à une exception près: les
dollars et les backslashes sont interprétés entre les guillemets. Exemple:
</p>
<pre>
<span class="prompt">chaland ~ $</span> echo "$HOME/*"
/users/87/maths/doligez/*</pre>
<p>
Une technique utile: Quand on juxtapose deux chaînes de caractères quotées, le
shell les concatène, et elles ne forment qu'un argument. Exemple:
</p>
<pre>
<span class="prompt">chaland ~ $</span> echo "'"'"'
'"</pre>
<p>
Quant aux interactions plus compliquées (backslashes à l'intérieur des
guillemets, guillemets à l'intérieur des apostrophes, etc.), le meilleur moyen
de savoir si ça donne bien le résultat attendu est d'essayer. La commande
<code>echo</code> est bien utile dans ce cas.
</p>
<h4>Les backquotes (<code>`</code>)</h4>
<p>
Dernière forme de quotation: <code>`<em>commande</em>`</code>. Le shell
exécute la <em>commande</em> indiquée entre backquotes, lit la sortie de la
commande mot par mot, et remplace <code>`</code> <em>commande</em>
<code>`</code> par la liste de ces mots. Exemple :
</p>
<pre>
<span class="prompt">chaland ~ $</span> echo `ls`
Mail News bin foo lib misc mur notes.aux notes.dvi notes.log
notes.tex planar text
<span class="prompt">chaland ~ $</span> ls -l `which emacs`
-rwxr-xr-t 1 root taff 978944 Jul 16 1991 /usr/local/bin/emacs</pre>
<p>
La commande <code>which <em>cmd</em></code> employée ci-dessus affiche sur sa
sortie le nom absolu du fichier exécuté par le shell quand on lance la
commande it <em>cmd</em> :
</p>
<pre>
<span class="prompt">chaland ~ $</span> which emacs
/usr/local/bin/emacs</pre>
<h3><a name="redirections">Redirections</a></h3>
<p>
Chaque commande a une <em>entrée standard</em>, une <em>sortie standard</em>,
et une <em>sortie d'erreur</em>. Par défaut, l'entrée standard est le clavier,
la sortie standard est l'écran, et la sortie d'erreur est aussi l'écran.
</p>
<h4>Rediriger la sortie dans un fichier : <code>&gt;</code></h4>
<p>
On peut <em> rediriger</em> la sortie standard d'une commande vers un fichier
(caractère <code>&gt;</code>). Le résultat de la commande sera placé dans le
fichier au lieu de s'afficher sur l'écran. Exemple:
</p>
<pre><span class="prompt">chaland ~ $</span> ls -l &gt; foo</pre>
<p>
Le résultat de <code>ls -l</code> ne s'affiche pas à l'écran, mais il est placé
dans le fichier <code>foo</code>. On peut alors taper
</p>
<pre><span class="prompt">chaland ~ $</span> less foo</pre>
<p class="continue">
(ou <code>more foo</code>)
pour lire le fichier page par page.
</p>
<h4>Rediriger l'entrée : <code>&lt;</code></h4>
<p>
On peut aussi rediriger l'entrée standard d'une commande (caractère
<code>&lt;</code>). La commande lira alors le fichier au lieu du clavier.
Exemple:
</p>
<pre><span class="prompt">chaland ~ $</span> elm leroy &lt; foo</pre>
<p class="continue">
envoie par mail à Xavier Leroy le résultat de la commande <code>ls -l</code> de
tout à l'heure.
</p>
<p>
On peut aussi taper <code>more &lt; foo</code> qui est équivalent à
<code>more foo</code> car <code>more</code> sans argument lit son entrée
standard et l'affiche page par page sur le terminal.
</p>
<h4>Connecter la sortie d'une commande sur l'entrée d'une autre :
<code>|</code></h4>
<p>
On peut se passer du fichier intermédiaire grâce à un <em>pipe</em>
(caractère <code>|</code>). Un pipe connecte directement la sortie standard d'une
commande sur l'entrée standard d'une autre commande. Exemple: pour afficher
page par page la liste des fichiers du répertoire courant, faire
</p>
<pre><span class="prompt">chaland ~ $</span> ls -l | less</pre>
<p>
Le pipe est d'un usage très courant et rend beaucoup de services.
</p>
<h4>Récapitulatif</h4>
<p>
La panoplie complète des redirections est la suivante (le tableau indique les
redirections qui diffèrent selon les shells) :
</p>
<ul>
<li><code>&gt;</code> : change la sortie standard de la commande pour la placer
dans un fichier.
</li>
<li><code>&lt;</code> : change l'entrée standard de la commande pour la prendre
dans un fichier.
</li>
<li><code>|</code> : branche la sortie standard de la commande de gauche sur
l'entrée standard de la commande de droite.
</li>
<li><code>&gt;&gt;</code> : change la sortie standard pour l'ajouter à la fin
d'un fichier existant.
</li>
<li><code>||</code> : exécuter la commande suivante si la première a
échoué.
</li>
<li><code>&amp;&amp;</code> : n'exécuter la commande suivante que si la
première a réussi.
</li>
</ul>
<table class="tableau">
<tr>
<th> Fonction </th>
<th> Bourne shell </th>
<th> Z-shell </th>
</tr>
<tr>
<td>Redirige la sortie d'erreur (2) et la sortie standard (1) sur l'entrée
de la commande suivante</td>
<td><code>2&gt;&amp;1 |</code></td>
<td><code> |&amp;</code></td>
</tr>
<tr>
<td>Redirige la sortie d'erreur et la sortie standard dans un fichier</td>
<td><code>2&gt;&amp;1 &gt;</code></td>
<td><code> &gt;&amp;</code></td>
</tr>
<tr>
<td>Redirige la sortie d'erreur et la sortie
standard à la fin d'un fichier existant</td>
<td><code>2&gt;&amp;1 &gt;&gt;</code></td>
<td><code>&gt;&gt;&amp;</code></td>
</tr>
</table>
<h4>Remarques</h4>
<p>
Normalement, une redirection avec <code>&gt;</code> sur un fichier qui
existe déjà efface le contenu du fichier avant d'y placer le résultat de la
commande. Les shells ont des options pour demander confirmation, ou
refuser d'effacer le fichier.
</p>
<p>
Une ligne de commandes contenant des <code>|</code> s'appelle un pipe-line.
Quelques commandes souvent utilisées dans les pipe-lines sont:
</p>
<ul>
<li><a href="fichiers.html#less">more</a> (ou <code>less</code>,
bien plus évolué) à la fin du pipe-line, affiche le résultat page par page,
pour laisser le temps de le lire.
</li>
<li><a href="divers.html#wc">wc</a> compte le nombre de
caractères, de mots et de lignes de son entrée.
</li>
<li><a href="chercher.html#grep">grep</a> cherche dans son
entre les lignes contenant un mot donné, et les écrit sur sa sortie.
</li>
<li><a href="filtres.html#sort">sort</a> lit toutes les lignes
de son entrée, les trie, et les écrit dans l'ordre sur sa sortie. Par défaut
l'ordre est alphabétique.
</li>
<li><a href="fichiers.html#tail">tail</a> écrit sur sa sortie
les dernières lignes de son entrée.
</li>
<li><a href="fichiers.html#head">head</a> écrit sur sa sortie
les premières lignes de son entrée.
</li>
<li><a href="fichiers.html#cat">cat</a> copie plusieurs fichiers
sur sa sortie.
</li>
<li><a href="filtres.html#fold">fold</a> coupe les lignes de son
entrée à 80 caractères et écrit le résultat sur sa sortie.
</li>
</ul>
<h4>Exemples</h4>
<pre>cat glop buz &gt; toto</pre>
<p>
Concatène les fichiers <code>glop</code> et <code>buz</code> et place le
résultat dans <code>toto</code>.
</p>
<pre>wc -w /usr/dict/words</pre>
<p>
Affiche le nombre de mots du dictionnaire Unix.
</p>
<pre>grep gag /usr/dict/words | tail</pre>
<p>
Affiche les 10 derniers mots du dictionnaire qui contiennent la chaîne
<code>gag</code>.
</p>
<h3><a name="variables">Variables</a></h3>
<p>
Le shell a des variables. Pour désigner le contenu d'une variable, on écrit
le nom de la variable précédé d'un dollar. Exemple: <code>echo $HOME</code>
affiche le nom du répertoire personnel de l'utilisateur.
</p>
<p>
La façon de donner une valeur à une variable varie selon le type de shell
utilisé :
</p>
<p>
<strong>C-Shell</strong> (<code>csh</code>, <code>tcsh</code>,
<code>lcsh</code>) : on utilise la commande <code>setenv</code> :
</p>
<pre>
<span class="prompt">chaland ~ $</span> setenv foo bar
<span class="prompt">chaland ~ $</span> echo $foo
bar</pre>
<p>
Famille des <strong>Bourne Shell</strong> (<code>sh</code>, <code>bash</code>,
<code>zsh</code>, <code>ksh</code>) : on utilise <code>export</code> :
</p>
<pre>
<span class="prompt">chaland ~ $</span> foo=bar
<span class="prompt">chaland ~ $</span> export foo
<span class="prompt">chaland ~ $</span> echo $foo
bar</pre>
<p>
Les valeurs des variables sont accessibles aux commandes lancées par le shell.
L'ensemble de ces valeurs constitue l'<em>environnement</em>. On peut aussi
supprimer une variable de l'environnement avec <code>unsetenv</code>
(C-Shell) ou <code>unset</code> (Bourne Shell).
</p>
<p>
Quelques variables d'environnement:
</p>
<ul>
<li><code>DISPLAY</code> : L'écran sur lequel les programmes X travaillent.
C'est souvent de la forme : <code>machine.somehost.somewhere:0.0</code>
Si c'est vide, c'est qu'il n'y a pas d'affichage graphique possible.
</li>
<li><code>PRINTER</code> : pour les commandes d'impression. Contient le nom de
l'imprimante sur laquelle il faut envoyer vos fichiers.
</li>
<li><code>EDITOR</code> : utilisée par <code>mutt</code>, <code>forum</code>,
et beaucoup d'autres commandes. Contient le nom de votre éditeur de textes
préféré.
</li>
<li><code>VISUAL</code> : la même chose qu'<code>EDITOR</code>.
</li>
<li><code>SHELL</code> : contient le nom de votre shell.
</li>
<li><code>HOME</code> : contient le nom de votre répertoire personnel.
</li>
<li><code>USER</code> : contient votre nom de login.
</li>
<li><code>LOGNAME</code> : la même chose que <code>USER</code>.
</li>
<li><code>PATH</code> : contient une liste de répertoires dans lesquels le
shell va chercher les commandes.
</li>
</ul>
<p>
Exercice : Assurez-vous que <code>/usr/local/games/bin</code> se trouve
bien dans votre PATH.
</p>
<h2><a name="programmation">Programmation du shell <code>sh</code></a></h2>
<p>
Un shell, quel qu'il soit, peut exécuter des commandes prises dans un
fichier. Un fichier contenant des commandes pour le shell est appelé un
<em>script</em>. C'est en fait un <em>programme</em> écrit <em>dans le
langage du shell</em>. Ce langage comprend non seulement les commandes que
nous avons déjà vues, mais aussi des structures de contrôle
(constructions conditionnelles et boucles).
</p>
<p>
Pour la programmation du shell, nous allons utiliser le shell <code>sh</code>,
qui est le plus répandu et standard. Ce que nous avons vu jusqu'ici
s'applique aussi bien à <code>sh</code> qu'à <code>zsh</code> et aussi à
<code>csh</code>, à l'exception de <code>setenv</code> et de certaines
redirections signalées. Pour être un script, un fichier doit commencer par
la ligne:
</p>
<pre>#!/bin/sh</pre>
<p>
Il doit aussi avoir être exécutable (bit <code>x</code>). Le
<code>#!/bin/sh</code> sur la première ligne indique que ce script doit être
exécuté par le shell <code>sh</code> dont on indique le chemin d'accès.
</p>
<h3><a name="structures">Structures de contrôle</a></h3>
<h4>for</h4>
<pre>
<code>for <em>var</em> in <em>liste de chaînes</em> ;
do <em>commandes</em> ; done</code></pre>
<p>
Affecte successivement à la variable de nom <em>var</em> chaque chaîne de
caractères trouvée dans la <em>liste de chaînes</em>, et exécute les
<em>commandes</em> une fois pour chaque chaîne.
</p>
<p>
Rappel : <code>$<em>var</em></code> accède à la valeur courante de
<em>var</em>. La partie <em>commandes</em> est une suite de commandes,
séparées par des <code>;</code> ou des retours à la ligne. (Tous les
<code>;</code> dans cette syntaxe peuvent aussi être remplacés par des
retours à la ligne.)
</p>
<p>
Exemple :
</p>
<pre>for i in *; do echo $i; done</pre>
<p class="continue">
affiche les noms de tous les fichiers du répertoire courant, un par ligne.
</p>
<h4>if</h4>
<pre>if <em>commande</em> ; then <em>commandes</em> ;
else <em>commandes</em> ; fi</pre>
<p>
Exécute l'une ou l'autre des listes de <em>commandes</em>, suivant que la
première <em>commande</em> a réussi ou non (voir ci-dessous).
</p>
<h4>while</h4>
<pre>while <em>commande</em> ; do <em>commande</em> ; done</pre>
<p>
Exécute les <em>commandes</em> de manière répétée tant que la première
<em>commande</em> réussit.
</p>
<h4>case</h4>
<pre>case <em>chaîne</em> in
<em>pattern</em>) <em>commande</em> ;;
<em>pattern</em>) <em>commande</em> ;;
esac</pre>
<p>
Exécute la première <em>commande</em> telle que la <em>chaîne</em> est de la
forme <em>pattern</em>. Un <em>pattern</em> est un mot contenant
éventuellement les constructions <code>*</code>, <code>?</code>,
<code>[a-d]</code>, avec la même signification que pour les raccourcis dans
les noms de fichiers. Exemple :
</p>
<pre>
case $var in
[0-9]*) echo 'Nombre';;
[a-zA-Z]*) echo 'Mot';;
*) echo 'Autre chose';;
esac</pre>
<h3><a name="retour">Code de retour</a></h3>
<p>
On remarque que la condition des commandes <code>if</code> et
<code>while</code> est une commande. Chaque commande renvoie un code de
retour (qui est ignoré en utilisation normale). Si le code est 0, la
commande a réussi; sinon, la commande a échoué. Par exemple, le compilateur
<code>cc</code> renvoie un code d'erreur non nul si le fichier compilé
contient des erreurs, ou s'il n'existe pas.
</p>
<p>
Les commandes <code>if</code> et <code>while</code> considèrent donc le code
de retour 0 comme « vrai », et tout autre code comme « faux ».
</p>
<p>
Il existe une commande <code>test</code>, qui évalue des expressions booléennes
passées en argument, et renvoie un code de retour en fonction du résultat.
Elle est bien utile pour les scripts. Exemple :
</p>
<pre>
if test $var = foo
then echo 'La variable vaut foo'
else echo 'La variable ne vaut pas foo'
fi</pre>
<h3><a name="shvariables">Variables</a></h3>
<p>
Dans les scripts, on peut utiliser des variables définies à l'extérieur
(avec <code>setenv</code> ou <code>export</code>), mais aussi définir ses
variables locales propres au script. On donne une valeur à une variable avec
une commande de la forme
<code><em>nom-de-variable</em>=<em>valeur</em></code>. Les variables sont
utilisées pour stocker des informations.
</p>
<p>
On a aussi des variables spéciales, initialisées automatiquement au
début du script:
</p>
<table class="tableau">
<tr>
<td><code>$0</code></td>
<td>Le nom de la commande (i.e. : du script)</td>
</tr>
<tr>
<td><code>$1</code>, <code>$2</code>, etc.</td>
<td>Le premier, deuxième, etc, argument passés au script.</td>
</tr>
<tr>
<td><code>$*</code></td>
<td>La liste de tous les arguments passés au script.</td>
</tr>
<tr>
<td><code>$#</code></td>
<td>Le nombre d'arguments passés au script.</td>
</tr>
<tr>
<td><code>$?</code></td>
<td>Le code de retour de la dernière commande lancée.</td>
</tr>
<tr>
<td><code>$!</code> </td>
<td>Le numéro de process de la dernière commande lancée en tâche de fond.</td>
</tr>
<tr>
<td><code>$$</code></td>
<td>Le numéro de process du shell lui-même.</td>
</tr>
</table>
<div class="metainformation">
Basé sur un polycopié de Roberto Di Cosmo, Xavier Leroy et Damien Doligez.
Ajustements : Nicolas George.
Dernière modification le 2002-11-16.
</div>
</body>
</html>