Ssreflect Users Discussion List

[Laurent Thery <>]

On 05/06/2014 07:29 PM, Beta Ziliani wrote:
> +1
>
> Actually, I think it would be much better to have a ssromega.  I have
> no idea how hard can it be to port omega to use ssrnat.
>
> Cheers,
> Beta
>
>
> On Tue, May 6, 2014 at 7:25 PM, Enrico Tassi <> wrote:
> > Hello, today I was asked if there is a bridge between the notions in
> > MathComp and the ones on which the "omega" tactic is able to work.
> >
> > I would not be surprised if someone already wrote a bunch of Ltac to do
> > the conversion.  If so, can you share it please?
> >
> > Cheers
> > --
> > Enrico Tassi

As a matter of fact I think it would be better to target lia that is 
more flexible than
omega. Frederic Besson told me that it should be not much
work but still I haven' t found time to do the job.

--
Laurent