X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fsequent2pres.ml;h=549f5c7c58d6437216b9c1d9320d19856938ee62;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=b1bc387581da31add8b68ac7879f3bebb605ce52;hpb=6abf435197c2bc37fadc0b3bd5925cd9cbe112e2;p=helm.git

diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml
index b1bc38758..549f5c7c5 100644
--- a/helm/software/components/content_pres/sequent2pres.ml
+++ b/helm/software/components/content_pres/sequent2pres.ml
@@ -102,12 +102,19 @@ let sequent2pres ~ids_to_inner_sorts =
        TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
       in
       CicNotationPres.box_of_mpres
-        (CicNotationPres.render ids_to_uris
+        (CicNotationPres.render
+          ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris)
           (TermContentPres.pp_ast ast)))
 
-let nsequent2pres ~subst =
+let nsequent2pres ~ids_to_nrefs ~subst =
+ let lookup_uri id =
+  try
+   let nref = Hashtbl.find ids_to_nrefs id in
+    Some (NReference.string_of_reference nref)
+  with Not_found -> None
+ in
   sequent2pres0
     (fun ast ->
       CicNotationPres.box_of_mpres
-       (CicNotationPres.render (Hashtbl.create 1)
+       (CicNotationPres.render ~lookup_uri
          (TermContentPres.pp_ast ast)))