-let decompose_tac ?(uris_choice_callback=(function l -> l)) term
- ~status:((proof,goal) as status)
-=
+(*
+let constructor_uri_of_string uri =
+ match cic_textual_parser_uri_of_string uri with
+ CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
+ | _ -> assert false
+;;
+
+let call_back uris =
+(* N.B.: nella finestra c'e' un campo "nessuno deei precedenti, prova questo" che non ha senso? *)
+(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
+(* domanda: due triple possono essere diverse solo per avere exp_named_subst diverse?? *)
+ let module U = UriManager in
+ List.map
+ (constructor_uri_of_string)
+ (!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)
+ )
+;;
+*)
+
+let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof,goal) as status) =