blob: 356f1e5b601de648f2329415a9c9bed1844292f9 (
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
34
35
36
|
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 ?
|
