X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationUtil.mli;h=ac291a2cebc72156afa5ffb44c54380a4a158832;hb=74c6905907b0bca229366d52450e2a6982b5b8be;hp=6194fc85558fa9e991ec7a120f7175903abc742e;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git diff --git a/matita/components/content/notationUtil.mli b/matita/components/content/notationUtil.mli index 6194fc855..ac291a2ce 100644 --- 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