X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=04440ffe7a75cefe1ce1b7d9315f2ef197928611;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=d3465d30a4e21d46b903f70ac0afa67df7c6990f;hpb=8161bcb58808e60658072bc3da83b62d1df2a223;p=helm.git diff --git a/matita/components/content_pres/cicNotationPres.ml b/matita/components/content_pres/cicNotationPres.ml index d3465d30a..04440ffe7 100644 --- a/matita/components/content_pres/cicNotationPres.ml +++ b/matita/components/content_pres/cicNotationPres.ml @@ -200,7 +200,7 @@ let add_parens child_prec curr_prec t = BoxPp.render_to_string (function x::_->x|_->assert false) ~map_unicode_to_tex:false 80 t);*)t) -let render ~lookup_uri ?(prec=(-1)) = +let render status ~lookup_uri ?(prec=(-1)) = let module A = Ast in let module P = Mpresentation in (* let use_unicode = true in *) @@ -309,7 +309,7 @@ let render ~lookup_uri ?(prec=(-1)) = | A.Magic _ | A.Variable _ -> assert false (* should have been instantiated *) | t -> - prerr_endline ("unexpected ast: " ^ NotationPp.pp_term t); + prerr_endline ("unexpected ast: " ^ NotationPp.pp_term status t); assert false and aux_attributes xmlattrs mathonly xref prec t = let reset = ref false in