- rewritesimpl_tac added in fourierR.ml (wrong location)

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index cbfe18e7360d497fdf2a65cc2fe4e5bde307b8cd..c980f723bf8d45fc264c3ff9918cd416b06edcc2 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -47,9 +47,9 @@ let htmlfooter =
  "</html>"
 ;;
 
-let prooffile = "/public/sacerdot/currentproof";;
+let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
 (*CSC: the getter should handle the innertypes, not the FS *)
-let innertypesfile = "/public/sacerdot/innertypes";;
+let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
 
 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 
@@ -684,8 +684,8 @@ let clear rendering_window =
 let fourier rendering_window =
  call_tactic ProofEngine.fourier rendering_window
 ;;
-let rewrite rendering_window =
- call_tactic_with_input ProofEngine.rewrite rendering_window
+let rewritesimpl rendering_window =
+ call_tactic_with_input ProofEngine.rewrite_simpl rendering_window
 ;;
 
 
@@ -746,7 +746,7 @@ let qed rendering_window () =
 (*????
 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
 *)
-let dtdname = "/projects/helm/V7/dtd/cic.dtd";;
+let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
 
 let save rendering_window () =
  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
@@ -1465,8 +1465,8 @@ class rendering_window output proofw (label : GMisc.label) =
  let fourierb =
   GButton.button ~label:"Fourier"
    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
- let rewriteb =
-  GButton.button ~label:"Rewrite ->"
+ let rewritesimplb =
+  GButton.button ~label:"RewriteSimpl ->"
    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
  let outputhtml =
   GHtml.xmhtml
@@ -1522,7 +1522,7 @@ object(self)
   ignore(clearbodyb#connect#clicked (clearbody self)) ;
   ignore(clearb#connect#clicked (clear self)) ;
   ignore(fourierb#connect#clicked (fourier self)) ;
-  ignore(rewriteb#connect#clicked (rewrite self)) ;
+  ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ;
   ignore(introsb#connect#clicked (intros self)) ;
   Logger.log_callback :=
    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
@@ -1534,7 +1534,7 @@ let rendering_window = ref None;;
 
 let initialize_everything () =
  let module U = Unix in
-  let output = GMathView.math_view ~width:400 ~height:280 ()
+  let output = GMathView.math_view ~width:350 ~height:280 ()
   and proofw = GMathView.math_view ~width:400 ~height:275 ()
   and label = GMisc.label ~text:"gTopLevel" () in
     let rendering_window' =