diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-08 13:56:32 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-08 13:56:32 +0000 |
| commit | 596ee07d61a2aa4a3f4acf0e3b2806d11f60695c (patch) | |
| tree | 6be6981067ad9645dd1a321c15b3bb3c4c8ab6db | |
| parent | cfba911ee7f12c68e24b2d8db2cee08d6c6713ff (diff) | |
changements dans les grammaires
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@58 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 039fcf210..2bdcfbc4a 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) + + |