o Discharge
     - conserver les constantes dans leur section de définition
       et redéfinir des constantes déchargées à la sortie

 o Variables existentielles
     - unifier Meta et Evar

 o Lib
     - écrire une fonction d'export qui supprimme les FrozenState,
       vérifie qu'il n'y a pas de section ouverte, et présente les
       déclarations dans l'ordre chronologique (y compris dans les
       sections fermées ?). A utiliser dans Library pour sauver un module.

 o configure
     - il faut tester la version du programme correspondant à $bytecamlc
       qui peut être ocamlc ou ocamlc.opt, et non pas la version de "ocamlc"
       seulement

 o Environnements compilés (type Environ.compiled_env)
     - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?)

 o Efficacité
     - utiliser DOPL plutôt que DOPN (sauf pour Case)
     - batch mode => pas de undo, ni de reset
     - conversion : déplier la constante la plus récente
     - un cache pour type_of_const, type_of_inductive, type_of_constructor,
       lookup_mind_specif

 o Lexer
     à compléter

 o Toplevel
     - parsing de la ligne de commande : utiliser Arg ?