New tactic rewrite implemented.

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

index 48c178918c019e9f6d3ad4ba1aac29d6ca8e9c7e..3c37b3ed268b67e2a57d62b00902cd8608b67d95 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -681,8 +681,13 @@ let clearbody rendering_window =
  let clear rendering_window =
   call_tactic_with_hypothesis_input ProofEngine.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 fourier rendering_window = call_tactic ProofEngine.fourier rendering_window;;
  
  
  let whd_in_scratch scratch_window =
@@ -1460,6 +1465,9 @@ 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"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
   let outputhtml =
    GHtml.xmhtml
     ~source:"<html><body bgColor=\"white\"></body></html>"
@@ -1514,6 +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(introsb#connect#clicked (intros self)) ;
    Logger.log_callback :=
     (Logger.log_to_html ~print_and_flush:(output_html outputhtml))