Ssreflect Users Discussion List

[Nicolas Magaud <>]

Dear all,

It surely will be very helpful to have a parametric omega tactic. In some 
recent work dealing with non standard arithmetic (in vanilla Coq), we faced 
the issues of proving some properties involving inequalities and omega was 
technically not available to ease our work: simply because our description of 
integers was an alternative (slightly different) to Z.

I’ll be happy to contribute in such an effort to improve the range of 
applications of all the available arithmetic tactics, for instance during the 
next Coq coding spring in early June.

Best regards,

Nicolas Magaud


> On 18 Feb 2016, at 13:24, Maxime Dénès 
> <>
>  wrote:
> 
> Hello,
> 
> On 02/18/16 12:21, Georges Gonthier wrote:
>> perhaps in the long run it might be better to parametrize omega with the 
>> theories it can work with
> 
> Yes, this is something I'd like to work on, once I am done with the more
> political issues that eat up my time these days.
> 
> Maxime.