aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/changements.txt
diff options
context:
space:
mode:
Diffstat (limited to 'dev/changements.txt')
-rw-r--r--dev/changements.txt14
1 files changed, 14 insertions, 0 deletions
diff --git a/dev/changements.txt b/dev/changements.txt
index 92251833f..538424d7f 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -71,3 +71,17 @@ Changements dans les grammaires
casse particulière dans Coq)
+Changements divers
+------------------
+
+ . il n'y a plus de script coqtop => coqtop et coqtop.byte sont
+ directement le résultat du link du code
+ => debuggage et profiling directs
+
+ . il n'y a plus d'installation locale dans bin/
+
+ . #use "include.ml" => #use "include"
+ go() => loop()
+
+ . il y "make depend" et "make dependcamlp4" car ce dernier prend beaucoup
+ de temps