]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/content/notationUtil.mli
Matitaweb:
[helm.git] / matitaB / components / content / notationUtil.mli
index 981030d49d8cc160e1a7f0245bcba4962f23e1a5..6d5919d93520306a1a7b5edc3748d9b2f313c8e4 100644 (file)
@@ -62,7 +62,7 @@ val visit_variable:
 val strip_attributes: NotationPt.term -> NotationPt.term
 
   (** @return the list of proper (i.e. non recursive) IdRef of a term *)
-val get_idrefs: NotationPt.term -> string list
+val get_idrefs: NotationPt.term -> (string * string option * string) list
 
   (** generalization of List.combine to n lists *)
 val ncombine: 'a list list -> 'a list list