transformations no longer use Content_expression, but rather CicAst

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

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index a2a010f7d0e925b812ed368e05e99d06b0320a90..1301d101772160ed78cd22e9899ea0d69ade1b41 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -53,7 +53,7 @@ let rec split n l =
   
 
 let is_big_general countterm p =
-  let maxsize = Cexpr2pres.maxsize in
+  let maxsize = Ast2pres.maxsize in
   let module Con = Content in
   let rec countp current_size p =
     if current_size > maxsize then current_size
@@ -126,7 +126,7 @@ let is_big_general countterm p =
   (size > maxsize)
 ;;
 
-let is_big = is_big_general (Cexpr2pres.countterm)
+let is_big = is_big_general (Ast2pres.countterm)
 ;;
 
 let get_xref =
@@ -834,10 +834,21 @@ let content2pres term2pres (id,params,metasenv,obj) =
       | _ -> raise ToDo
 ;;
 
+(*
 let content2pres ~ids_to_inner_sorts =
  content2pres 
   (function p -> 
      (Cexpr2pres.cexpr2pres_charcount 
                    (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
 ;;
+*)
+
+let content2pres ~ids_to_inner_sorts =
+  content2pres
+    (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)