-
Sylvain Dailler authored
Added proof_state and functions to control it in controller_itp. Tried to add a test case for it inside the command p to put a big P next to a goal that is proved. It is currently buggy. Needs investigating and cleaning.
8ed16ca6