X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=b9e89769472371c31b3a27e4ae8beedf1db53c49;hb=488f49d2ac60fa63e65a19ad8684414266e05ac6;hp=477697580fd4df83314ad345634a798b47870237;hpb=d83abd7e5e107f75b24e45dc75ad859ebc11c0fa;p=helm.git diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 477697580..b9e897694 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -960,7 +960,7 @@ let content2pres content2pres ?skip_initial_lambdas ?skip_thm_and_qed (fun ?(prec=90) annterm -> let ast, ids_to_uris = - TermAcicContent.ast_of_acic ids_to_inner_sorts annterm + TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in CicNotationPres.box_of_mpres (CicNotationPres.render ids_to_uris ~prec