Is there a tactic like `Show Proof.`

but that tells you the theorem qualid? Similarly is there one which tells you the theorem statement for which you are proving? Obviously these are not normal requests as this information is visible to the user. This is for data extraction inside Serapi. (In Lean I know how to easily write a tactic to get this data, but not in Coq.)

Jason Rute has marked this topic as resolved.

Last updated: Sep 30 2023 at 06:01 UTC