]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationUtil.mli
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.mli
index 80e36524225339c3ab6f2fe05e7bd3d23d17f2c6..ad16a2eb6ca459d095db0a0fd1b23d27320e4b01 100644 (file)
@@ -54,6 +54,9 @@ val visit_variable:
 
 val strip_attributes: CicNotationPt.term -> CicNotationPt.term
 
+  (** @return the list of proper (i.e. non recursive) IdRef of a term *)
+val get_idrefs: CicNotationPt.term -> string list
+
   (** generalization of List.combine to n lists *)
 val ncombine: 'a list list -> 'a list list