- let asequent,ids_to_terms,
- ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses =
- Cic2acic.asequent_of_sequent metasenv sequent in
+ let unsh_sequent,(asequent,ids_to_terms,
+ ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
+ =
+ Cic2acic.asequent_of_sequent metasenv sequent
+ in