]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/content_pres/sequent2pres.ml
More parts of the lexicon status made functional.
[helm.git] / matita / components / content_pres / sequent2pres.ml
index 7951dbf5d158fda66f828f1b394d3ce618bbff40..53e8e19b49ac1a0b85a991871eb85ba91c45e766 100644 (file)
@@ -95,7 +95,7 @@ let sequent2pres0 term2pres (_,_,context,ty) =
        Box.b_space; 
        pres_goal]))])
 
-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
@@ -106,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)))