Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 22 insertions, 0 deletions

diff --git a/dev/TODO b/dev/TODO
new file mode 100644
index 00000000..926861c9
--- /dev/null
+++ b/dev/TODO
@@ -0,0 +1,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 ???
+
+