we rebuilt the dependences

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

diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml
index d9c3a325e808a7d531dddd37d2a9be124ff1a967..b1bc387581da31add8b68ac7879f3bebb605ce52 100644 (file)
--- a/helm/software/components/content_pres/sequent2pres.ml
+++ b/helm/software/components/content_pres/sequent2pres.ml
@@ -47,7 +47,7 @@ let b_ink a = Box.Ink a
 module K = Content
 module P = Mpresentation
 
-let sequent2pres term2pres (_,_,context,ty) =
+let sequent2pres0 term2pres (_,_,context,ty) =
    let context2pres context = 
      let rec aux accum =
      function 
@@ -96,7 +96,7 @@ let sequent2pres term2pres (_,_,context,ty) =
        pres_goal]))])
 
 let sequent2pres ~ids_to_inner_sorts =
-  sequent2pres
+  sequent2pres0
     (fun annterm ->
       let ast, ids_to_uris =
        TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
@@ -105,3 +105,9 @@ let sequent2pres ~ids_to_inner_sorts =
         (CicNotationPres.render ids_to_uris
           (TermContentPres.pp_ast ast)))
 
+let nsequent2pres ~subst =
+  sequent2pres0
+    (fun ast ->
+      CicNotationPres.box_of_mpres
+       (CicNotationPres.render (Hashtbl.create 1)
+         (TermContentPres.pp_ast ast)))