]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationUtil.mli
added XmlAttrs attribute for specification of xml attributes directly
[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.mli
index 1a7d7d6f4e4d5c0cc7527acae5dc573f86016f1c..fd7e12f7f6a1ae0d26f3c6cc296546e05b209fb2 100644 (file)
@@ -28,6 +28,9 @@ val fresh_name: unit -> string
 val variables_of_term: CicNotationPt.term -> CicNotationPt.pattern_variable list
 val names_of_term: CicNotationPt.term -> string list
 
+  (** extract all keywords (i.e. string literals) from a level 1 pattern *)
+val keywords_of_term: CicNotationPt.term -> string list
+
 val visit_ast:
   ?special_k:(CicNotationPt.term -> CicNotationPt.term) ->
   (CicNotationPt.term -> CicNotationPt.term) ->
@@ -51,3 +54,5 @@ val boxify: CicNotationPt.term list -> CicNotationPt.term
 val find_appl_pattern_uris:
   CicNotationPt.cic_appl_pattern -> UriManager.uri list
 
+val find_branch:
+  CicNotationPt.term -> CicNotationPt.term