The Coq mailing list

[Ryan Wisnesky <ryan AT cs.harvard.edu>]

Such a conversion could be non-trivial in that to avoid reifying the syntax 
of Prop, it would probably need to be a tactic (although you could use 
explicit syntax), and regardless, it would require heavy use of a classical 
logic axiom or a decidable domain.  It would be pretty useful though, so I 
hope it exists.

On Sep 3, 2012, at 6:20 PM, Marko Maliković 
<marko AT ffri.hr>
 wrote:

> Regards,
> 
> Is there module for conversion first-order formulas over the Prop into
> Prenex form. I can not find it.
> 
> Great thanks,
> 
> -----------------------
> Dr. Sc. Marko Maliković
> Docent
> Filozofski fakultet
> Sveučilište u Rijeci
> ---------------------
> Ph.D. Marko Maliković
> Assistant Professor
> Faculty of Humanities and Social Sciences
> University of Rijeka, Croatia
> -----------------------------
> marko.malikovic AT ffri.hr
> http://www.ffri.hr/~marko
> -------------------------