Pour utiliser Coq sur votre machine personnelle, il faut disposer
- d'une version récente de Coq, au moins 8.9.0 ;
  la version actuelle, janvier 2021, est 8.13.0. 
- et d'une interface permettant à la fois d'éditer un fichier et d'effectuer
  des commandes Coq. Deux possibilités :
  -- coqide
  -- emacs avec proofgeneral

Des informations générales sur l'installation de Coq sont ici : https://coq.inria.fr/

Des instructions pour installer un environnement complet (sur linux) comprenant
emacs, OCaml et Coq sont ici :
https://ltpf.gricad-pages.univ-grenoble-alpes.fr/commun/installation/install.html

La procédure ci-dessus passe par un système de packages OCaml appelé opam, et a été utilisée
récemment avec succès par une promotion d'étudiants de Polytech.

Il est possible d'installer Coq par d'autres moyens, voir  https://coq.inria.fr/

Ensuite, pour avoir l'environnement de λ-calcul non typé 

- récupérer untypedLC.v.gz dans le répertoire "secours",
  frère du répertoire courant, puis
$ gunzip untypedLC.v.gz
$ coqc untypedLC.v

Cela fournit un fichier untypedLC.vo qui doit se trouver dans le répertoire
d'ooù vous lancez coq (soit via coqide, soit via emacs, soit directement via coqtop
pour un usage très très basique).