blob: 68f0474261705298b8f1aff826f02e51a2f47634 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
o warning camlp4
<W> Changing associativity of level "<top>"
� comprendre et supprimmer
(on peut faire Grammar.warning_verbose := False, mais il vaut mieux
comprendre)
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 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 Toplevel
- parsing de la ligne de commande : utiliser Arg ???
|
