Added Decompose tactic

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index ebe26c3e350a915089f1dbe229547d1620bdee0d..f590481baf7ed79d7a9acd70a807bd3467c7958e 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -352,6 +352,9 @@ let
    raise NoChoice
 ;;
 
+EliminationTactics.interactive_user_uri_choice :=
+ (fun ~selection_mode -> interactive_user_uri_choice ~selection_mode:selection_mode);;
+
 let interactive_interpretation_choice interpretations =
  let chosen = ref None in
  let window =
@@ -2148,9 +2151,7 @@ let assumption = call_tactic ProofEngine.assumption;;
 let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
 let absurd = call_tactic_with_input ProofEngine.absurd;;
 let contradiction = call_tactic ProofEngine.contradiction;;
-(* Galla chiede: come dare alla tattica la lista di termini da decomporre?
-let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;;
-*)
+let decompose = call_tactic_with_input ProofEngine.decompose;;
 
 let whd_in_scratch scratch_window =
  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
@@ -3083,6 +3084,9 @@ object(self)
    let searchpatternb =
     GButton.button ~label:"SearchPattern_Apply"
      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+   let decomposeb =
+    GButton.button ~label:"Decompose"
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
 
    ignore(exactb#connect#clicked exact) ;
    ignore(applyb#connect#clicked apply) ;
@@ -3118,6 +3122,7 @@ object(self)
    ignore(introsb#connect#clicked intros) ;
    ignore(searchpatternb#connect#clicked searchPattern) ;
    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
+   ignore(decomposeb#connect#clicked decompose) ;
   ))
 end
 ;;