- (*
- let _, (acic_sequent, _, _, ids_to_inner_sorts, _) =
- Cic2acic.asequent_of_sequent metasenv cic_sequent in
- let _, _, _, annterm = acic_sequent in
- let ast, ids_to_uris =
- TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in
- let pped_ast = TermContentPres.pp_ast ast in
- let markup = CicNotationPres.render ids_to_uris pped_ast in
- BoxPp.render_to_string text_width markup
- *)
- ApplyTransformation.txt_of_cic_sequent_conclusion
- text_width metasenv cic_sequent
-
- method private pattern_of term context unsh_sequent =
- let context_len = List.length context in
+ let map_unicode_to_tex =
+ Helm_registry.get_bool "matita.paste_unicode_as_tex" in
+ ApplyTransformation.txt_of_cic_sequent_conclusion ~map_unicode_to_tex
+ ~output_type text_width metasenv cic_sequent
+
+ method private pattern_of term father_hyp unsh_sequent =