Assia Mahboubi
Assia Mahboubi
Hi @bshvass. Thanks for resurrecting this topic. Indeed, I have some Ltac code that makes the ring tactic operational for the `rat` type in a robust way, that can also...
Hi @bshvass, thanks for resurrecting this topic. Indeed, this is an old known issue... @CohenCyril is right, a few years ago I wrote some Ltac code for making the `ring`...
@spitters I think this topic deserves a specific issue...
Hello, for the record, there is a prototype [here](https://github.com/amahboubi/lia4mathcomp). It should work fine with current mathcomp.
The archive of the mailing list has another thread about this issue. [Here](https://sympa.inria.fr/sympa/arc/ssreflect/2016-02/msg00046.html) is the relevant message in which I mentioned the previous repository
@ggonthier should this be done before the upcoming release or can it wait for the next one?
Agreed, thanks.
Hello @MrSet! Thanks for contributing! These two lemmas are indeed interesting ones, although there are a few issues of the way they are phrased that should be discussed before they...
@CohenCyril , it's great to see progress on this front! Could you update the header comment so as to make the roadmap clearer? In particular, it seems that fixpoints-related material...
I am trying to understand the roadmap for this PR. How do you see it?