On Fri, 2009-02-20 at 15:43 +0100, whoami314@free.fr wrote: > Hi > > This ITP is a nice idea. In my research group, we're now using csdp > as an external oracle when solving inequalities in the Coq proof assistant > (see [1], or more specifically [2] for the use of csdp in Coq). This > coinor-cdsp package could simplify things quite a bit for us, by becoming > a "recommends" or "suggests" or whatever for package coq. Anyway, if you need > early testers, or even help during the creation of this package, let me know... > > Best regards, > > Pierre Letouzey (Coq development team) > letouzey AT pps.jussieu.fr > > [1]: http://packages.debian.org/coq > [2]: http://www.irisa.fr/lande/fbesson/Fast_Reflexive_Arithmetics_Tactics.pdf Sure, but you should carefully check whether licenses (coinor uses CLP) are compatible and maybe askt on the coinor mailinglist if they can give an exception in case there is a problem... Soeren
Attachment:
signature.asc
Description: This is a digitally signed message part