(sprintf "Exception raised during the refresh of the sequent: %s"
(Printexc.to_string e))));
ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
(sprintf "Exception raised during the refresh of the sequent: %s"
(Printexc.to_string e))));
ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->