diff options
| -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 |