+ if List.length metasenv = 0 then
+ begin
+ !qed_set_sensitive true ;
+prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.clear ()" ;
+ Hbugs.clear ()
+ end
+ else
+begin
+prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.notify ()" ;
+ Hbugs.notify () ;
+end ;