[Why3-club] GUI - "obsolete" status makes "context all goals" necessary

João Paulo Carvalho joao_paulo_c at yahoo.com
Sun Feb 19 18:04:17 CET 2012


In WHY3 Interactive Proof Session, if you have an unproved goal which has a interactive proof session marked as "obsolete", and your "Context" is marked as "Unproved goals", then button "Replay" is innocuous. You have to mark "Context" as "All goals" to make button "Replay" workable.

For an unproved goal, click at an "interactive prover button" (as Coq), edit it, and then you get an "obsolete" proof session.

João Paulo.

More information about the Why3-club mailing list