update in bsasic_2

[helm.git] / matita / components / content / notationUtil.mli

diff --git a/matita/components/content/notationUtil.mli b/matita/components/content/notationUtil.mli
index 6194fc85558fa9e991ec7a120f7175903abc742e..ac291a2cebc72156afa5ffb44c54380a4a158832 100644 (file)
--- a/matita/components/content/notationUtil.mli
+++ b/matita/components/content/notationUtil.mli
@@ -76,15 +76,11 @@ val group: NotationPt.term list -> NotationPt.term
 val ungroup: NotationPt.term list -> NotationPt.term list
 
 val find_appl_pattern_uris:
-  NotationPt.cic_appl_pattern ->
-   [`Uri of UriManager.uri | `NRef of NReference.reference] list
+  NotationPt.cic_appl_pattern -> NReference.reference list
 
 val find_branch:
   NotationPt.term -> NotationPt.term
 
-val cic_name_of_name: NotationPt.term -> Cic.name
-val name_of_cic_name: Cic.name -> NotationPt.term
-
   (** Symbol/Numbers instances *)
 
 val freshen_term: NotationPt.term -> NotationPt.term
@@ -96,3 +92,7 @@ type notation_id
 
 val fresh_id: unit -> notation_id
 
+val refresh_uri_in_term:
+ refresh_uri_in_term:(NCic.term -> NCic.term) ->
+ refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
+  NotationPt.term -> NotationPt.term