Unified: refactoring

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

diff --git a/helm/software/components/content_pres/objPp.ml b/helm/software/components/content_pres/objPp.ml
index 68badf3242e3514b406c2deb76cf551bc5720061..3cdad5528a56dac0b13021fa9f743b74d95ee02b 100644 (file)
--- a/helm/software/components/content_pres/objPp.ml
+++ b/helm/software/components/content_pres/objPp.ml
@@ -32,7 +32,8 @@ let term2pres n ids_to_inner_sorts annterm =
    in
    let bobj =
       CicNotationPres.box_of_mpres (
-         CicNotationPres.render ids_to_uris (TermContentPres.pp_ast ast)
+         CicNotationPres.render ~prec:90 ids_to_uris 
+           (TermContentPres.pp_ast ast)
       )
    in
    let render = function _::x::_ -> x | _ -> assert false in
@@ -41,7 +42,12 @@ let term2pres n ids_to_inner_sorts annterm =
    remove_closed_substs s
 
 let obj_to_string n style prefix obj =
-  let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = Cic2acic.acic_object_of_cic_object obj in
+  let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = 
+     try Cic2acic.acic_object_of_cic_object obj
+     with e -> 
+        let msg = "Cic2ACic: " ^ Printexc.to_string e in
+       failwith msg
+  in
   match style with
      | GrafiteAst.Declarative ->
         let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in