Il faut avoir préalablement installé Coq en suivant par exemple
les instructions données dans 

<http://www-verimag.imag.fr/~monin/Enseignement/LTPF/robuste/commun/installation/install.html>

Ces instructions permettent en fait d'installer un environnement plus
complet comprenant, en dehors de coq et de l'interface coqide
(disponibles aussi sur les machine IM2AG), une autre interface
pour emacs appelée proof-general ainsi que le langage OCaml.

Le présent répertoire contient un fichier coq à utiliser
pour expérimenter du λ-calcul non typé en Coq.
Attention, vous devez disposer d'une version de Coq
suffisamment récente (8.9 ou suivantes).
Ce n'est pas forcément le cas de la version de Coq fournie
par les paquetages de Debian ou Ubuntu.
Il faut au final obtenir un fichier untypedLC.vo
(du coq préalablement compilé) dans le répertoire de travail.

Différents formats sont proposés :

- à la racine, la version source (ainsi qu'une version compressée 
  par gzip en cas de pbs avec les accents)
  à compiler chez soi par la commande :

  `coqc untypedLC.v`

   (quelques warnings sans importance sont émis).
   
- sous les répertoires `Version_compilee_XXX`, une version précompilée
  pour différentes versions de Coq (la version du compilateur OCaml utilisé 
  semble significative aussi, à partir de coq_8.15.)


```
Version html de cette page produite par :
pandoc -s --metadata pagetitle="MCAL λ README install" -o README.html README.md
```