X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationUtil.ml;h=3683c0c0e80383996751eb6c6858c31f552cd179;hb=606dab57f31b66eb3f30f603185124b88dfad4c1;hp=52abe456442dd097152a9f5e8c54f6dca9568755;hpb=0d2bfb98d8343b4e6cefdb506a813b7cb5749630;p=helm.git

diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml
index 52abe4564..3683c0c0e 100644
--- a/matita/components/content/notationUtil.ml
+++ b/matita/components/content/notationUtil.ml
@@ -328,21 +328,13 @@ let dressn ~sep:sauces =
 let find_appl_pattern_uris ap =
   let rec aux acc =
     function
-    | Ast.UriPattern uri -> `Uri uri :: acc
-    | Ast.NRefPattern nref -> `NRef nref :: acc
+    | Ast.NRefPattern nref -> nref :: acc
     | Ast.ImplicitPattern
     | Ast.VarPattern _ -> acc
     | Ast.ApplPattern apl -> List.fold_left aux acc apl
   in
   let uris = aux [] ap in
-  let cmp u1 u2 =
-   match u1,u2 with
-      `Uri u1, `Uri u2 -> UriManager.compare u1 u2
-    | `NRef r1, `NRef r2 -> NReference.compare r1 r2
-    | `Uri _,`NRef _ -> -1
-    | `NRef _, `Uri _ -> 1
-  in
-  HExtlib.list_uniq (List.fast_sort cmp uris)
+  HExtlib.list_uniq (List.fast_sort NReference.compare uris)
 
 let rec find_branch =
   function
@@ -394,14 +386,30 @@ let freshen_obj obj =
           indtypes
       in
       NotationPt.Inductive (freshen_capture_variables params, indtypes)
-  | NotationPt.Theorem (flav, n, t, ty_opt,p) ->
+  | NotationPt.Theorem (n, t, ty_opt, attrs) ->
       let ty_opt =
         match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
       in
-      NotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
+      NotationPt.Theorem (n, freshen_term t, ty_opt, attrs)
   | NotationPt.Record (params, n, ty, fields) ->
       NotationPt.Record (freshen_capture_variables params, n,
         freshen_term ty, freshen_name_ty_b fields)
 
 let freshen_term = freshen_term ?index:None
 
+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)
+;;