X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=72f51c5f8acf261a9b453bf9f0aebeb7adf88cb3;hp=d9255f220d02247026943886f1515e96d1194a27;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hpb=ede00573e3e4cb28df7ca9a5dae6228c2b432608

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index d9255f220..72f51c5f8 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -1061,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