Ssreflect Users Discussion List

[Laurent Thery <>]

On 05/06/2014 07: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

My idea was not to depend of ZArith. So to do the reification and the 
verification of
the certificate directly in ssrint but maybe I am a bit naive.

--
Laurent