X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=7dc1e2357c7c30bc86db0ba94eac9f3e8376ddeb;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=05e4ae3cbd8d55532a9cb51ba41b3324989f8389;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 05e4ae3cb..7dc1e2357 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 -> 'b)
   (id,params,metasenv,obj) 
 =
   match obj with
@@ -1070,7 +1071,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 -> 'b)
   (id,params,metasenv,obj : CicNotationPt.term Content.cobj) 
 =
   match obj with