coercion lookup now returns coercions ranked using the number of symbols matched...

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

diff --git a/matita/components/content_pres/sequent2pres.ml b/matita/components/content_pres/sequent2pres.ml
index 549f5c7c58d6437216b9c1d9320d19856938ee62..53e8e19b49ac1a0b85a991871eb85ba91c45e766 100644 (file)
--- 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)))