diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-06 16:09:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-06 16:09:03 +0000 |
| commit | 794567cd3d35d40b4ad4a4d7a1b0e11e38c4f257 (patch) | |
| tree | 2805fd4a87b772e59dff2305ca14ee2e80509e76 /CHANGES | |
| parent | 970b4b750486ad8544b5d0a3b2246282690e6c98 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@674 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 5 |
1 files changed, 4 insertions, 1 deletions
@@ -8,6 +8,9 @@ - Correction de bugs (quand le type ne commence pas par un inductif) - Simpl ne déplie plus les appels récursifs d'un Fix mutuel réduit + Il réduit un peu plus aussi (source d'incompatibilité). + +- Davantage d'inférence automatique de "?". - Les cas des Cases ne se lisent plus de manière séquentielle, sauf en cas de clauses par défaut redondantes auquel cas la première est prise @@ -30,4 +33,4 @@ l'ast, il faut typer explicitement la grammaire avec Ast ou List - Ajout d'un Let primitif -- Ajout (officiel) d'une tactique LetTac et d'un Induction "convivial"
\ No newline at end of file +- Ajout (officiel) d'une tactique LetTac et d'un Induction "convivial" |