X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Fengine.ml;h=324d114a949302b28788952074f9962714b80871;hb=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0;hp=83de453f733993275e73d7024a037015b8e3fc77;hpb=28e8954fbe2e28f01ae918c8d0e0ef34bd84b48f;p=helm.git diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 83de453f7..324d114a9 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -26,6 +26,7 @@ module K = Kernel module T = TeX module O = TeXOutput module A = Anticipate +module M = Meta module N = Alpha type status = { @@ -63,7 +64,9 @@ let mk_ptr st name = let get_macro s l = let rec aux = function - | [] -> "", 0 + | [] -> + if !G.log_missing then missing s l; + "", 0 | (r, m, a, x) :: _ when r = s && a = l -> m, x | _ :: tl -> aux tl in @@ -75,9 +78,7 @@ let get_head = function let l = L.length ts in let macro, x = get_macro s l in begin match macro with - | "" -> - if !G.log_missing then missing s l; - None + | "" | "APPL" -> None | _ -> let ts1, ts2 = X.split_at x ts in @@ -131,7 +132,11 @@ let rec proc_term st is = function proc_sort st is s | C.Const c -> let s, name = K.resolve_reference c in - T.Macro "GREF" :: T.arg (mk_gname name) :: T.free s :: is + let macro, _ = get_macro s 0 in + if macro = "" || macro = "APPL" then + T.Macro "GREF" :: T.arg (mk_gname name) :: T.free s :: is + else + T.Macro macro :: T.free s :: is | C.Match (w, u, v, ts) -> let is_w = proc_term st [] (C.Const w) in let is_u = proc_term st [] u in @@ -262,10 +267,14 @@ let open_out_tex s = open_out (F.concat !G.out_dir fname) let proc_pair s ss u = function - | None -> + | None -> + let text_u = + if K.not_prop1 [] u then proc_item "assumption" + else proc_item "axiom" + in let name = X.rev_map_concat X.id "." "type" ss in let och = open_out_tex name in - O.out_text och (proc_item "axiom" s name u); + O.out_text och (text_u s name u); close_out och | Some t -> let text_u, text_t =