diff options
| -rw-r--r-- | CHANGEMENTS | 8 | ||||
| -rw-r--r-- | PROBLEMES | 4 | ||||
| -rwxr-xr-x | tools/translate_V6-3-1_to_V7-0 | 17 |
3 files changed, 23 insertions, 6 deletions
diff --git a/CHANGEMENTS b/CHANGEMENTS index e3f6b85eb..74bf08679 100644 --- a/CHANGEMENTS +++ b/CHANGEMENTS @@ -23,6 +23,10 @@ Langage La syntaxe du "." final change (cf Vernac). Le nommage des définitions globales change (cf Métathéorie). +- Le problème avec les identificateurs se terminant par un nombre + supérieur à 2^30 est résolu. + +- Le caractère "$" n'est plus autorisé dans les identificateurs. Extensions de syntaxe avec Grammar et Syntax @@ -79,7 +83,7 @@ Syntaxe des constructions Commandes -- Changement de noms de certaines commandes +- Changement de nom de certaines commandes AddPath -> Add LoadPath; Print LoadPath -> Print LoadPath; @@ -135,7 +139,7 @@ Tactiques d'un tel language et se procurer une documentation provisoire de Ltac, se référer à l'URL suivante: - http://pauillac.inria.fr/~delahaye/ + http://logical.inria.fr/~delahaye/ - Tactique Let renommé en LetTac et utilise le let-in primitif; Induction renommé en OldInduction et nouveau Induction plus @@ -91,8 +91,8 @@ Nijmegen OK Paris/ZF OK Sophia-Antipolis/Cours-de-Coq -File "./ps.v", line 206, characters 3-31 -Error: A is already used +File "./Partial_order_facts.v", line 123, characters 3-96 +Error: Not an inductive product Sophia-Antipolis/HARDWARE ?? Sophia-Antipolis/MATHS ?? Sophia-Antipolis/condom ... vide diff --git a/tools/translate_V6-3-1_to_V7-0 b/tools/translate_V6-3-1_to_V7-0 index 4e49a9026..10e7f1403 100755 --- a/tools/translate_V6-3-1_to_V7-0 +++ b/tools/translate_V6-3-1_to_V7-0 @@ -1,8 +1,21 @@ #! /bin/sh -echo Insertion of a space after a dot not followed by a separator +echo "This shell script performs the following transformations:" +echo "- Insertion of a space after a dot not followed by a separator" +echo "- Insertion of a space between consecutive ~ and < and between" +echo " consecutive | and < assumed to be part of distinct tokens" +echo "- Various renamings of commands as described in document Changes.ps" + for i in $* - do sed -e "s/\.\([A-Z]\)/\. \1/g" -e "s/AddPath$i/Add LoadPath/g" > $i.tmp$$ + do sed -e "s/\.\([A-Z]\)/\. \1/g" -e "s/AddPath/Add LoadPath/g" \ + -e "s/~</~ </g" -e "s/|</| </g" \ + -e "s/AddPath/Add LoadPath/g" -e "s/DelPath/Remove LoadPath/g" \ + -e "s/AddRecPath/Add Rec LoadPath/g" \ + -e "s/Implicit *Arguments *On/Set Implicit Arguments/g" \ + -e "s/Implicit *Arguments *Off/Unset Implicit Arguments/g" \ + -e "s/Begin *Silent/Set Silent/g" -e "s/End *Silent/Unset Silent/g" \ + -e "s/Print *Path/Print Coercion Paths/g" \ + $i > $i.tmp$$ if diff $i.tmp$$ $i > /dev/null then rm $i.tmp$$ |