X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2Fsequent2pres.ml;h=53e8e19b49ac1a0b85a991871eb85ba91c45e766;hb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;hp=549f5c7c58d6437216b9c1d9320d19856938ee62;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/content_pres/sequent2pres.ml b/matita/components/content_pres/sequent2pres.ml
index 549f5c7c5..53e8e19b4 100644
--- a/matita/components/content_pres/sequent2pres.ml
+++ b/matita/components/content_pres/sequent2pres.ml
@@ -95,18 +95,7 @@ let sequent2pres0 term2pres (_,_,context,ty) =
        Box.b_space; 
        pres_goal]))])
 
-let sequent2pres ~ids_to_inner_sorts =
-  sequent2pres0
-    (fun annterm ->
-      let ast, ids_to_uris =
-       TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
-      in
-      CicNotationPres.box_of_mpres
-        (CicNotationPres.render
-          ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris)
-          (TermContentPres.pp_ast ast)))
-
-let nsequent2pres ~ids_to_nrefs ~subst =
+let nsequent2pres status ~ids_to_nrefs ~subst =
  let lookup_uri id =
   try
    let nref = Hashtbl.find ids_to_nrefs id in
@@ -117,4 +106,4 @@ let nsequent2pres ~ids_to_nrefs ~subst =
     (fun ast ->
       CicNotationPres.box_of_mpres
        (CicNotationPres.render ~lookup_uri
-         (TermContentPres.pp_ast ast)))
+         (TermContentPres.pp_ast status ast)))