transformations no longer use Content_expression, but rather CicAst

[helm.git] / helm / ocaml / cic_transformations / sequent2pres.ml

diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml
index 2b159e1c898736b759af10bf4bbc3affc9f10060..57d7d9140a9868d147147cd49774b0ce710732c2 100644 (file)
--- a/helm/ocaml/cic_transformations/sequent2pres.ml
+++ b/helm/ocaml/cic_transformations/sequent2pres.ml
@@ -92,13 +92,22 @@ 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 =
+prerr_endline "Sequent2pres.sequent2pres";
+  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)