]> 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 1fd57e0d00cdcec44e1fb2c7059cc42ea2b32bbf..def5b0a1bb9a6834d24d60d61cce87bcbad2072a 100644 (file)
@@ -23,6 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
+
   (** {2 Persistant state handling} *)
 
 type interpretation_id
@@ -53,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 *)