]> matita.cs.unibo.it Git - helm.git/blobdiff - components/content_pres/sequent2pres.mli
Pretty-printing of "match ... with" pattern syntax fixed. We need an
[helm.git] / components / content_pres / sequent2pres.mli
index 615c8e35f2cc5be590e0a0346db3c269b613d6d8..d6d9daa4005918fbe6892eb920679190e940492d 100644 (file)
@@ -36,4 +36,3 @@ val sequent2pres :
   ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
   Cic.annterm Content.conjecture ->
     CicNotationPres.boxml_markup
-