The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Le 09/10/2016 à 21:23, Gregory Malecha a écrit :
> I have thought a bit about implementing something like Knuth-Bendix on 
> top of it, but I have not really started implementing it beyond a 
> little bit of sketching. Personally, I think that it would be 
> extremely useful to the community.

Hi. For completion, I would rather suggest to reuse existing 
(specialized) tools producing certificates that can be verified. See for 
instance http://cl-informatik.uibk.ac.at/software/kbcv/ which produces 
CPF certificates that can be certified by 
http://cl-informatik.uibk.ac.at/software/ceta/ . Best regards, Frédéric.