+ | RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+prerr_endline "PROVA CHE FA SOLLEVARE UN'ECCEZIONE:" ; flush stderr ;
+begin
+match !ProofEngine.proof with Some (_,metasenv,bo,_) ->
+List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^
+CicPp.ppterm ty) ; flush stderr) metasenv ;
+prerr_endline ("PROOF: " ^ CicPp.ppterm bo) ; flush stderr ;
+end ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output