-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.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
- 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 ~term ~status:((proof,goal) as status) =