X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=72f51c5f8acf261a9b453bf9f0aebeb7adf88cb3;hb=513c4a61f11ce03888a8a0f9d8e513de6e3a7c8b;hp=05e4ae3cbd8d55532a9cb51ba41b3324989f8389;hpb=38ec119c163b0e6f97a9800933d5b71c065332e8;p=helm.git

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 05e4ae3cb..72f51c5f8 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -1013,7 +1013,8 @@ let njoint_def2pres term2pres joint_kind defs =
 ;;
 
 let content2pres0
-  ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
+  ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+  (term2pres : ?prec:int -> 'a)
   (id,params,metasenv,obj) 
 =
   match obj with
@@ -1060,6 +1061,7 @@ let content2pres
   ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts 
 =
   content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
+(* FG: prec not optional in my patch *)
     (fun ?(prec=90) annterm ->
       let ast, ids_to_uris =
        TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
@@ -1070,7 +1072,8 @@ let content2pres
           (TermContentPres.pp_ast ast)))
 
 let ncontent2pres0
-  ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
+  ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+  (term2pres : ?prec:int -> 'a)
   (id,params,metasenv,obj : CicNotationPt.term Content.cobj) 
 =
   match obj with