Stream: Coq devs & plugin devs

Topic: admit-like tactic


view this post on Zulip Chantal Keller (Jul 21 2020 at 10:44):

Hello
I am developping an OCaml tactic that should behave like admit: admit the current goal, and force to finish the proof with Admitted. I believe it is sufficient to directly use the already existing admit tactic? If so, in which .mli file can I find it?
Thanks!

view this post on Zulip Pierre-Marie Pédrot (Jul 21 2020 at 10:58):

It's Proofview.give_up.

view this post on Zulip Chantal Keller (Jul 21 2020 at 10:59):

thanks!


Last updated: Oct 13 2024 at 01:02 UTC