diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/changements.txt | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/dev/changements.txt b/dev/changements.txt new file mode 100644 index 0000000000..5a190073fa --- /dev/null +++ b/dev/changements.txt @@ -0,0 +1,10 @@ + +Voici les changements d'organisation / modules : + + AVANT APRÈS + ================================ =============================== + Std, More_util lib/util.ml + + Names kernel/names.ml et kernel/sign.ml + (les parties noms et signatures ont été séparées) + |