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 dclaration (dans Declare)
et stocker cette information dans le in_variable, in_constant, etc.
o Environnements compils (type Environ.compiled_env)
- pas de timestamp mais plutt un checksum avec Digest (mais comment ?)
o Efficacit
- utiliser DOPL plutt que DOPN (sauf pour Case)
- batch mode => pas de undo, ni de reset
- conversion : dplier la constante la plus rcente
- 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 ???
|
