X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent%2FnotationUtil.mli;h=6d5919d93520306a1a7b5edc3748d9b2f313c8e4;hb=2f19651bcec24abfb1bf15ff7e1387daad1f6638;hp=ac291a2cebc72156afa5ffb44c54380a4a158832;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/content/notationUtil.mli b/matitaB/components/content/notationUtil.mli
index ac291a2ce..6d5919d93 100644
--- a/matitaB/components/content/notationUtil.mli
+++ b/matitaB/components/content/notationUtil.mli
@@ -33,6 +33,7 @@ val keywords_of_term: NotationPt.term -> string list
 
 val visit_ast:
   ?special_k:(NotationPt.term -> NotationPt.term) ->
+  ?clear_interpretation:bool ->
   ?map_xref_option:(NotationPt.href option -> NotationPt.href option) ->
   ?map_case_indty:(NotationPt.case_indtype option ->
           NotationPt.case_indtype option) ->
@@ -61,12 +62,13 @@ 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
 
 val string_of_literal: NotationPt.literal -> string
+val html_of_literal: NotationPt.literal -> string 
 
 val dress:  sep:'a -> 'a list -> 'a list
 val dressn: sep:'a list -> 'a list -> 'a list