X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fsequent2pres.ml;h=afd2292ba0bfe7b8823151d2485980ca4a8b3337;hb=fdd8107cc53f5e862004aa5fcd48593ee5634234;hp=2b159e1c898736b759af10bf4bbc3affc9f10060;hpb=9ab5ca8acba80b19a939eea2cd87761507e7128b;p=helm.git

diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml
index 2b159e1c8..afd2292ba 100644
--- a/helm/ocaml/cic_transformations/sequent2pres.ml
+++ b/helm/ocaml/cic_transformations/sequent2pres.ml
@@ -92,13 +92,21 @@ let sequent2pres term2pres (_,_,context,ty) =
      pres_goal])
 ;;
 
+(*
 let sequent2pres ~ids_to_inner_sorts =
  sequent2pres 
   (function p -> 
    (Cexpr2pres.cexpr2pres_charcount 
     (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
 ;;
+*)
 
-
-
+let sequent2pres ~ids_to_inner_sorts =
+  sequent2pres
+    (fun annterm ->
+      let (ast, ids_to_uris) as arg =
+        Acic2Ast.ast_of_acic ids_to_inner_sorts annterm
+      in
+      let astbox = Ast2pres.ast2astBox arg in
+      Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astbox)