bugfix update in basic_2

[helm.git] / matita / components / content_pres / cicNotationPres.ml

diff --git a/matita/components/content_pres/cicNotationPres.ml b/matita/components/content_pres/cicNotationPres.ml
index 5f9f202caeaf09b8d7b299444018106abe8a6062..04440ffe7a75cefe1ce1b7d9315f2ef197928611 100644 (file)
--- a/matita/components/content_pres/cicNotationPres.ml
+++ b/matita/components/content_pres/cicNotationPres.ml
@@ -200,14 +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 lookup_uri ids_to_uris id =
- try
-   let uri = Hashtbl.find ids_to_uris id in
-   Some (NReference.string_of_reference uri)
- with Not_found -> None
-;;
-
-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 *)
@@ -316,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