diff options
| author | herbelin | 2001-12-21 18:39:37 +0000 |
|---|---|---|
| committer | herbelin | 2001-12-21 18:39:37 +0000 |
| commit | 91d0724e4a88911dd81c20bd5a858272b7372194 (patch) | |
| tree | f579fca70bb7d7138be0b70618eb8c0e02f7a593 | |
| parent | e65b8c257454a7409844f3ac64b91596f00f80f3 (diff) | |
Extension de Even
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2368 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 8 |
1 files changed, 3 insertions, 5 deletions
@@ -9,7 +9,7 @@ Language - Coercions allowed in Cases patterns - New declaration "Canonical Structure id = t : I" to help resolution of equations of the form (proj ?)=a; if proj(e)=a then a is canonically - equipped with the remaining fields in e, i.e. ? is instantantiated by e + equipped with the remaining fields in e, i.e. ? is instantiated by e Tactics @@ -18,14 +18,12 @@ Tactics - Slight improvement in naming strategy for NewInduction/NewDestruct - Intuition/Tauto do not perform useless unfolding and work up to conversion -Extraction +Extraction (details in contrib/extraction/CHANGES or documentation) -See contrib/extraction/CHANGES or documentation. In brief: - Syntax changes: there are no more options inside the extraction commands. New commands for customization and options have been introduced instead. - More optimizations on extracted code. -- Extraction tests are now embbeded in 14 user contributions. - +- Extraction tests are now embedded in 14 user contributions. Standard library |