C.output_html
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e ^ "</h1>") ;
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e ^ "</h1>") ;
None -> assert false
| Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
in
None -> assert false
| Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
in
| Some t -> (C.term_editor ())#set_term t);
(C.term_editor ())#get_metasenv_and_term canonical_context metasenv
in
| Some t -> (C.term_editor ())#set_term t);
(C.term_editor ())#get_metasenv_and_term canonical_context metasenv
in
- ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+ ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e ^ "</h1>") ;
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal
let call_tactic_with_goal_input tactic () =
let module L = LogicalOperations in
let module G = Gdome in
ProofEngine.goal := savedgoal
let call_tactic_with_goal_input tactic () =
let module L = LogicalOperations in
let module G = Gdome in
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of " ^
"the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of " ^
"the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of " ^
"the proof: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of " ^
"the proof: " ^ Printexc.to_string e ^ "</h1>") ;
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e ^ "</h1>") ;
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal
let call_tactic_with_input_and_goal_input tactic () =
let module L = LogicalOperations in
let module G = Gdome in
ProofEngine.goal := savedgoal
let call_tactic_with_input_and_goal_input tactic () =
let module L = LogicalOperations in
let module G = Gdome in
None -> assert false
| Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
in
None -> assert false
| Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
in
- ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+ ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of " ^
"the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of " ^
"the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of " ^
"the proof: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of " ^
"the proof: " ^ Printexc.to_string e ^ "</h1>") ;
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of " ^
"the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of " ^
"the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of " ^
"the proof: " ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("<h1 color=\"red\">Exception raised during the refresh of " ^
"the proof: " ^ Printexc.to_string e ^ "</h1>") ;