The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

This has been discussed a while back:
https://sympa.inria.fr/sympa/arc/coq-club/2020-10/msg00004.html


On Fri, 2021-01-08 at 12:47 -0800, Abhishek Anand wrote:
> I see that there is a field instance for Qc.
> Is there a psatz/lra like tactic for Qc?
> If not, is there a tactic to preprocess a Qc goal to Q, something
> like what zify does? (Thanks Frédéric for solving the problem in the
> other thread.)
> 
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/