]> matita.cs.unibo.it Git - helm.git/blobdiff - components/content_pres/content2pres.ml
Pretty-printing of "match ... with" pattern syntax fixed. We need an
[helm.git] / components / content_pres / content2pres.ml
index 477697580fd4df83314ad345634a798b47870237..b9e89769472371c31b3a27e4ae8beedf1db53c49 100644 (file)
@@ -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