]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationUtil.mli
snapshot
[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.mli
index b5e242b7fca86f80fdce7a277c080b7100ca5d24..92eaf8e8b5857003ebd127506a6f30d1373afd68 100644 (file)
@@ -25,6 +25,9 @@
 
 val fresh_name: unit -> string
 
+val variables_of_term: CicNotationPt.term -> CicNotationPt.pattern_variable list
+val names_of_term: CicNotationPt.term -> string list
+
 val visit_ast:
   ?special_k:(CicNotationPt.term -> CicNotationPt.term) ->
   (CicNotationPt.term -> CicNotationPt.term) ->