- let
- (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
- ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
- =
- Cic2acic.acic_object_of_cic_object obj
- in
- let mml =
- ChosenTransformer.mml_of_cic_object
- ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types
+ let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures,
+ ids_to_hypotheses,_,_)) =
+ ApplyTransformation.mml_of_cic_object obj