X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationUtil.ml;h=3d80e8fd51427a0d091335a95e186b1b4553d91f;hb=d4f2d4c1a4784f84aa27e1bb96b8b377a6553c65;hp=a2ab34833cd098ea72335c56d9242c2ec60498cf;hpb=791d52ba005e434be27cca1f8059d9f28da0183b;p=helm.git

diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml
index a2ab34833..3d80e8fd5 100644
--- a/matita/components/content/notationUtil.ml
+++ b/matita/components/content/notationUtil.ml
@@ -397,4 +397,19 @@ let freshen_obj obj =
 
 let freshen_term = freshen_term ?index:None
 
-let refresh_uri_in_term t = assert false
+let rec refresh_uri_in_term ~refresh_uri_in_term:refresh_in_cic
+ ~refresh_uri_in_reference
+=
+ function
+    NotationPt.NRef ref -> NotationPt.NRef (refresh_uri_in_reference ref)
+  | NotationPt.NCic t -> NotationPt.NCic (refresh_in_cic t)
+  | t ->
+     visit_ast
+     (refresh_uri_in_term ~refresh_uri_in_term:refresh_in_cic
+       ~refresh_uri_in_reference) t
+      ~special_k:(fun x -> x)
+      ~map_xref_option:(function Some ref -> Some (refresh_uri_in_reference ref)
+                         | x -> x)
+      ~map_case_indty:(function (Some (s,Some ref)) -> Some (s, Some
+                        (refresh_uri_in_reference ref)) | x -> x)
+;;