diff options
| author | courant | 2001-09-13 07:36:23 +0000 |
|---|---|---|
| committer | courant | 2001-09-13 07:36:23 +0000 |
| commit | 13e17eac2e476114305472e581a433d8c08d48d6 (patch) | |
| tree | 4c5c23c3b488b2ea076361afbe3ea019538f1eb9 | |
| parent | b5e4be1a483f7667b2f1d55db75bb30a2a589cf2 (diff) | |
explications modifications Tauto
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1956 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -1,5 +1,9 @@ Modifications depuis la V7.0 +- Tauto considère de façon uniforme les égalités : un but contenant des + égalités de la forme "t=t" sera résolu de la même façon que si toutes + ces égalités étaient remplacées par "True". En particulier, Tauto résout + tous les buts de la forme "H : ~ t = t |- A". - Fonctions de réduction dans les définitions locales s'appliquent par défaut au corps de la définition. Extension de la notion de Clause pour forcer l'action sur le type des défs seulement sous la forme |