diff options
| author | barras | 2006-11-02 13:59:14 +0000 |
|---|---|---|
| committer | barras | 2006-11-02 13:59:14 +0000 |
| commit | 87229783dd5ad20e16129f577efb1f94358231ac (patch) | |
| tree | b8ad0d49baadd1a75a12d8004e37858350beaddf /CHANGES | |
| parent | c4b2e6587c536b00d76ab98df80c1c8a18d0bd0b (diff) | |
gestion speciale du niveau 5 des ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9333 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 9 |
1 files changed, 5 insertions, 4 deletions
@@ -21,7 +21,9 @@ Language and commands Tactics -- Improved implementation of the ring and field tactics. +- Improved implementation of the ring and field tactics. For compatibility + reasons, the previous tactics are renamed as legacy ring and legacy field, + but should be considered as deprecated. - New declarative mathematical proof language. - Support for argument lists of arbitrary length in Tactic Notation. - [rewrite ... in H] now fails if [H] is used either in an hypothesis @@ -90,9 +92,8 @@ Tactics setoid_symmetry, setoid_transitivity, setoid_reflexivity and autorewite). New syntax for declaring relations and morphisms (old syntax still working with minor modifications, but deprecated). -- New implementation of the ring tactic with a built-in notion of coefficients - and a better usage of setoids. Previous implementation kept for compatibility - but is deprecated. +- New implementation (still experimental) of the ring tactic with a built-in + notion of coefficients and a better usage of setoids. - New conversion tactic "vm_compute": evaluates the goal (or an hypothesis) with a call-by-value strategy, using the compiled version of terms. - When rewriting H where H is not directly a Coq equality, search first H for |