diff options
| author | herbelin | 2001-09-09 10:58:15 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-09 10:58:15 +0000 |
| commit | 9443a73eac29ffe946a552cae7ece055ff20d5fb (patch) | |
| tree | fae81c7fdf3662a15f8db3e16a5209f6ce524f78 | |
| parent | 42c154399403a55766116b7b46968e20e00967f6 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1932 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 13 |
1 files changed, 11 insertions, 2 deletions
@@ -20,12 +20,21 @@ Modifications depuis la V7.0 être suivies d'une métavariable, idem pour { }) - Développeur: les var des ast sont maintenant des identifiers - Les identificateurs ne sont plus mutables +- Inversion, Injection, Discriminate, ... font des intros until +- Decompose supprime les hypothèses temporaires - Nouvelle tactique Assert qui fait la coupure du calcul des séquents (et dans le sens attendu) -- Inversion peut faire des Intros until avant - Amélioration de l'efficacité de l'ancien Cut -- En cas de Require en milieu de section, les noms courts importes par le module disparaissent a la fermeture de la section, +- En cas de Require en milieu de section, les noms courts importes par + le module disparaissent a la fermeture de la section, et les Require ultérieurs ne les réintroduisent pas. +- NewInduction et NewDestruct sont maintenant achevés: elles unifient + Elim et Induction, et Case et Destruct en proposant un comportement plus + "naturel" (par rapport au Induction de la V6 qui s'applique sur les + hypothèses du contexte, la stratégie de nommage est + différente). Elim et Case restent nécessaires pour les cas où + l'hypothèse d'élimination est un produit sur un type inductif. + Différences oubliées dans la V7.0beta : |