]> matita.cs.unibo.it Git - helm.git/blobdiff - components/content_pres/sequent2pres.ml
Pretty-printing of "match ... with" pattern syntax fixed. We need an
[helm.git] / components / content_pres / sequent2pres.ml
index 2ae090bb01e1d2f0a0040c21fa7d162bdacde7c4..d9c3a325e808a7d531dddd37d2a9be124ff1a967 100644 (file)
@@ -99,7 +99,7 @@ let sequent2pres ~ids_to_inner_sorts =
   sequent2pres
     (fun 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