Ssreflect Users Discussion List

[François Pottier <>]

Hi Laurent,

Thanks for your reply; this is helpful.

> You can still perform an adhoc translation with Ltac but I guess this is not > what you are looking for

I think this is what I am looking for, especially if someone has already
written this piece of Ltac and if it handles all of the arithmetic operators
and logical connectives known to "omega". Does such a thing exist? It seems
that (for certain kinds of proofs) it would be a pity to work without "omega".

--
François Pottier

http://gallium.inria.fr/~fpottier/