Decompose now has a new parameter which is the callback to call to select the

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 9d1b3e982969625da635f395361938b5f5be9500..396c968fd99e170eb100854f0bd3c0f341bc41bd 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -352,9 +352,6 @@ 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 =
@@ -1814,6 +1811,23 @@ let check scratch_window () =
       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
+let decompose_uris_choice_callback uris = 
+(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
+  let module U = UriManager in 
+   List.map 
+    (function uri ->
+      match Disambiguate.cic_textual_parser_uri_of_string uri with
+         CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
+       | _ -> assert false)
+    (interactive_user_uri_choice 
+      ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false 
+      ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" 
+      (List.map 
+        (function (uri,typeno,_) ->
+          U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)
+        ) uris)
+    ) 
+;;
 
 (***********************)
 (*       TACTICS       *)
@@ -2156,7 +2170,9 @@ 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;;
-let decompose = call_tactic_with_input ProofEngine.decompose;;
+let decompose =
+ call_tactic_with_input
+  (ProofEngine.decompose ~uris_choice_callback:decompose_uris_choice_callback);;
 
 let whd_in_scratch scratch_window =
  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch