Distribution:

- Faire fonctionner coqc/coqtop en non local

Environnement:

- Faire fonctionner Search
- Faire fonctionner Abstract
- Faire fonctionner Reset
- Que les Infix soit chargés lors d'un Require
- Problème de compatibilité du mode implicite au discharge (avant, dépendait
  de l'état du mode à la création, maintenant, à la fermeture de la section)

Tactiques

- Choisir la précédence de Try/Orelse
- Éviter si possible les '(

Noyau:

- Intégrer Let dans whd_* et les fonctions de tacred