Fourier tactic

[helm.git] / helm / gTopLevel / gTopLevel.ml
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml

index bf2918593fb04b63a4058befa1b334c072b5c93e..1a4e6ce65be5230979a62104db7ee913c4d17f5f 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -47,9 +47,9 @@ let htmlfooter =
   "</html>"
  ;;
  
-let prooffile = "/home/galata/miohelm/currentproof";;
+let prooffile = "/home/tassi/miohelm/currentproof";;
  (*CSC: the getter should handle the innertypes, not the FS *)
-let innertypesfile = "/home/galata/miohelm/innertypes";;
+let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
  
  (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
  
@@ -682,6 +682,8 @@ let clear rendering_window =
   call_tactic_with_hypothesis_input ProofEngine.clear rendering_window
  ;;
  
+let fourier rendering_window = call_tactic ProofEngine.fourier rendering_window;;
+
  
  let whd_in_scratch scratch_window =
   call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
@@ -1428,6 +1430,9 @@ class rendering_window output proofw (label : GMisc.label) =
   let clearb =
    GButton.button ~label:"Clear"
     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let fourierb =
+  GButton.button ~label:"Fourier"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
   let outputhtml =
    GHtml.xmhtml
     ~source:"<html><body bgColor=\"white\"></body></html>"
@@ -1481,6 +1486,7 @@ object(self)
    ignore(ringb#connect#clicked (ring self)) ;
    ignore(clearbodyb#connect#clicked (clearbody self)) ;
    ignore(clearb#connect#clicked (clear self)) ;
+  ignore(fourierb#connect#clicked (fourier self)) ;
    ignore(introsb#connect#clicked (intros self)) ;
    Logger.log_callback :=
     (Logger.log_to_html ~print_and_flush:(output_html outputhtml))