summaryrefslogtreecommitdiff
path: root/dev/TODO
blob: 926861c9659b8bad9ac236ba678e80587506b6e2 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

 o options de la ligne de commande
     - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml

 o arguments implicites
     - les calculer une fois pour toutes � la d�claration (dans Declare)
       et stocker cette information dans le in_variable, in_constant, etc.

 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 Toplevel
     - parsing de la ligne de commande : utiliser Arg ???