The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Hello!

On http://color.inria.fr, you will find a new release of CoLoR, a Coq 
Library on Rewriting and termination.

Among the main new features since the last release on March 11, you will 
find:

- the use of N. Dershowitz's improvement for computing dependency pairs,

- the basic flat context closure transformation,

- a formalization of semantic labelling with models or quasi-models, and 
infinite or finite sets of rules,

- root labelling, a particular case of semantic labelling,

- collapsing argument filterings (non-collapsing argument filterings 
were already formalized),

- a loop checker for (relative) TRSs or SRSs,

- non-termination when the variable condition is not satisfied,

- the conversion into SRSs of TRSs with unary symbols only,

- signature morphisms and their properties wrt termination,

- semi-rings, matrices and matrix interpretations now operate on setoids,

- a syntactic matching algorithm proved correct and complete,

- positions in a term,

- the list of reducts of a term,

- a translation of CoLoR terms into Coccinelle terms 
(http://a3pat.ensiie.fr/).

You can browse the definitions and lemmas on 
http://color.inria.fr/doc/main.html.

Enjoy!