parameter sintax added to axiom statement

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

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index d9255f220d02247026943886f1515e96d1194a27..72f51c5f8acf261a9b453bf9f0aebeb7adf88cb3 100644 (file)
--- 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