-let mml_of_cic_term metano term =
- let metasenv =
- match !ProofEngine.proof with
- None -> []
- | Some (_,metasenv,_,_) -> metasenv
- in
- let context =
- match !ProofEngine.goal with
- None -> []
- | Some metano ->
- let (_,canonical_context,_) =
- List.find (function (m,_,_) -> m=metano) metasenv
- in
- canonical_context
- in
- let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
- SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
- in
- let sequent_doc =
- Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome
- in
- let res = apply_sequent_stylesheets sequent_doc in
- res, (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
+let mml_of_cic_sequent metasenv sequent =
+ let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
+ SequentPp.XmlPp.print_sequent metasenv sequent in
+ let sequent_doc =
+ Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome in
+ let sequent_mml = apply_sequent_stylesheets sequent_doc in
+ sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses)