Ssreflect Users Discussion List

[Maxime Dénès <>]

I've always wondered (because I'm not using these things a lot), is 
there any reason to prefer omega over romega?

As to how to interface it, I guess the clean way to go would be to 
re-express these tactics over typeclasses supporting the required 
equational reasoning, as is now done for ring... Then supporting it in 
SSR would just be a matter of defining a typeclass instance.

Maxime.

On 05/06/2014 01:52 PM, Enrico Tassi wrote:
> On Tue, May 06, 2014 at 07:35:32PM +0200, Laurent Thery wrote:
> > 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.
> For lia we have something to/from ssrint in the proof of Apery actually,
> but is not bullet proof, it is an Ltac hack.  You had something cleaner
> in mind?
>
> Ciao