X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationUtil.mli;h=fd7e12f7f6a1ae0d26f3c6cc296546e05b209fb2;hb=ba2dfe6409e95bf9e558dc0d4be382b068671409;hp=a03c415d2b5ee9f5b9f2c7e97171dd67521058ca;hpb=7aa0e7901b71a660c6d6f55d96a38a3a9d1d3c7d;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli
index a03c415d2..fd7e12f7f 100644
--- a/helm/ocaml/cic_notation/cicNotationUtil.mli
+++ b/helm/ocaml/cic_notation/cicNotationUtil.mli
@@ -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) ->