Ana de Almeida Borges (Sep 27 2020 at 19:03): Ana de Almeida Borges (Sep 27 2020 at 19:03):I have a Program Fixpoint definition that generates two obligations and is able to automatically prove one of them.
However, it takes a long time to do so, and I could probably prove it manually without much effort.
Is there a way to prevent Program Fixpoint to try to automatically prove the obligations?
Yannick Zakowski (Sep 27 2020 at 19:06):You can change the tactic that gets run to solve the obligations, so I guess setting it locally to idtac would do the trick?
https://coq.github.io/doc/v8.12/refman/addendum/program.html?highlight=program%20fixpoint#coq:cmd.obligation-tactic
Kenji Maillard (Sep 27 2020 at 19:06):Set the obligation tactic so that it gives up eagerly on your goal, for instance Obligation Tactic := idtac.; if you want to prevent only some of the goals from being solved by the obligation tactic, you can also use a variation of what's presented there.
Ana de Almeida Borges (Sep 27 2020 at 19:10):Cool! Setting Local Obligation Tactic := intros. is slightly more useful than idtac and does the trick. Thank you :)
Last updated: Sep 25 2023 at 12:01 UTC