Distribution:

- Faire fonctionner coqc/coqtop en non local

Environnement:

- Faire fonctionner Search
- Faire fonctionner Abstract
- Faire fonctionner Reset
- Faire fonctionner Transparent/Opaque
- Ajouter "parsing" aux chemins par défaut (pour g_{nat,z}syntax.cmo)

- Que les Infix soit chargés lors d'un Require (DONE)
- Problème de compatibilité du mode implicite au discharge (DONE)

Tactiques

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

Noyau:

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

Theories:

- remplacer Realizer par Refine ou autre chose dans TheoryList.v