"matita.paste_unicode_as_tex")
~skip_thm_and_qed:true
~skip_initial_lambdas:how_many_lambdas
- 80 GrafiteAst.Declarative "" obj
+ 80 [] obj
else
if true then
(* use cic2grafite *)
Helm_registry.get_bool "matita.paste_unicode_as_tex"
in
ApplyTransformation.procedural_txt_of_cic_term
- ~map_unicode_to_tex 78 cc proof_term
+ ~map_unicode_to_tex 78 [] cc proof_term
in
let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in
[],text,parsed_text_length
ProofEngineTypes.Fail _ as exn ->
raise exn
(* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
- | TA.Inline (_,style,suri,prefix,flavour) ->
+ | TA.Inline (_, suri, params) ->
let str = "\n\n" ^
ApplyTransformation.txt_of_inline_macro
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
- style ?flavour prefix suri
+ params suri
in
[], str, String.length parsed_text