(UriManager.uri * int * 'b list) list
val mk_fresh_name_callback :
Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
- (* invoked when the proof assistant's status has changed to notify Hbugs *)
- val notify_hbugs : unit -> unit
end
;;
try
tactic () ;
C.refresh_goals () ;
- C.refresh_proof () ;
- C.notify_hbugs ()
+ C.refresh_proof ()
with
RefreshSequentException e ->
C.output_html
tactic expr ;
C.refresh_goals () ;
C.refresh_proof () ;
- (C.term_editor ())#reset ;
- C.notify_hbugs ()
+ (C.term_editor ())#reset
with
RefreshSequentException e ->
C.output_html
try
tactic term ;
C.refresh_goals () ;
- C.refresh_proof () ;
- C.notify_hbugs ()
+ C.refresh_proof ()
with
RefreshSequentException e ->
C.output_html
tactic terms ;
C.refresh_goals () ;
C.refresh_proof () ;
- C.notify_hbugs ()
with
RefreshSequentException e ->
C.output_html
tactic ~goal_input:term ~input:expr ;
C.refresh_goals () ;
C.refresh_proof () ;
- (C.term_editor ())#reset ;
- C.notify_hbugs ()
+ (C.term_editor ())#reset
with
RefreshSequentException e ->
C.output_html
try
tactic hypothesis ;
C.refresh_goals () ;
- C.refresh_proof () ;
- C.notify_hbugs ()
+ C.refresh_proof ()
with
RefreshSequentException e ->
C.output_html