diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/changements.txt | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/dev/changements.txt b/dev/changements.txt index 039fcf210f..2bdcfbc4a3 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -2,15 +2,12 @@ Changements d'organisation / modules : -------------------------------------- - AVANT APRÈS - ================================ =============================== - Std, More_util lib/util.ml + Std, More_util -> lib/util.ml - Names kernel/names.ml et kernel/sign.ml + Names -> kernel/names.ml et kernel/sign.ml (les parties noms et signatures ont été séparées) - Changements dans les types de données : --------------------------------------- dans Generic: free_rels : constr -> int Listset.t @@ -20,6 +17,7 @@ Changements dans les types de données : environment -> context context -> typed_type signature + Changements dans les fonctions : -------------------------------- @@ -55,3 +53,13 @@ Changements dans les fonctions : type_of_type -> type_of_sort fcn_proposition -> type_of_type + +Changements dans les grammaires +------------------------------- + + . le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex + + . attention : LIDENT -> IDENT (les identificateurs n'ont pas de + casse particulière dans Coq) + + |