]> matita.cs.unibo.it Git - helm.git/blobdiff - components/acic_content/termAcicContent.mli
Pretty-printing of "match ... with" pattern syntax fixed. We need an
[helm.git] / components / acic_content / termAcicContent.mli
index 49358bfce00a8b546e71c787b1afc1c68fbaa4b6..def5b0a1bb9a6834d24d60d61cce87bcbad2072a 100644 (file)
@@ -54,6 +54,7 @@ val set_active_interpretations: interpretation_id list -> unit
   (** {2 acic -> content} *)
 
 val ast_of_acic:
+  output_type:[`Pattern|`Term] ->
   (Cic.id, CicNotationPt.sort_kind) Hashtbl.t ->    (* id -> sort *)
   Cic.annterm ->                                    (* acic *)
     CicNotationPt.term                              (* ast *)