X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=4fa7d9e5f5389fb0c148de50a5672b2c86c4e5f1;hb=4ed8829233095bdf2ab1c15021ba815084d19b70;hp=34ca16d256e5460fd24f2f00d6b93d60e57abf87;hpb=3b3a14912c135dc45da970d71235b630660d88c8;p=helm.git diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 34ca16d25..4fa7d9e5f 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -561,25 +561,11 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status cic2grafite cc menv proof_term else (* alternative using FG stuff *) - let proof_term, how_many_lambdas = - Auto.lambda_close ~prefix_name:"orrible_hack_" - proof_term menv cc - in - let ty,_ = - CicTypeChecker.type_of_aux' - menv [] proof_term CicUniv.empty_ugraph - in - let obj = - Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma]) - in - Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+" - (strip_comments - (ApplyTransformation.txt_of_cic_object - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - ~skip_thm_and_qed:true - ~skip_initial_lambdas:how_many_lambdas - 80 (GrafiteAst.Procedural None) "" obj)) + let map_unicode_to_tex = + Helm_registry.get_bool "matita.paste_unicode_as_tex" + in + ApplyTransformation.procedural_txt_of_cic_term + ~map_unicode_to_tex 78 cc proof_term in let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in [],text,parsed_text_length