Huge commit with several changes:

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index fadc551056f350ad8ad01e7f96c1e25041d66cfc..b221919d2e33a38433f3216bcb3498718541c06a 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -346,8 +346,8 @@ let cic2grafite context menv t =
     let width = max_int in
     let term_pp content_term =
       let pres_term = TermContentPres.pp_ast content_term in
-      let dummy_tbl = Hashtbl.create 1 in
-      let markup = CicNotationPres.render dummy_tbl pres_term in
+      let lookup_uri = fun _ -> None in
+      let markup = CicNotationPres.render ~lookup_uri pres_term in
       let s = "(" ^ BoxPp.render_to_string
        ~map_unicode_to_tex:(Helm_registry.get_bool
          "matita.paste_unicode_as_tex")