X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=df29edc3b7421049ec63eb5a4616560fbfcb07fd;hb=842919f2f8ee71a5301ad962220569450340a9e9;hp=6573e39822f991840d8cbca78fce0779d336de8b;hpb=d4ace1a2d7b08813af331e33efb499bcea4888f5;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 6573e3982..df29edc3b 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -32,16 +32,17 @@ open MatitaTypes
 let extract_alias types uri = 
   fst(List.fold_left (
     fun (acc,i) (name, _, _, cl) -> 
-      ((name, UriManager.string_of_uriref (uri,[i]))
+      (name, UriManager.string_of_uri (UriManager.uri_of_uriref uri i None))
       ::
       (fst(List.fold_left (
         fun (acc,j) (name,_) ->
-          (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
-        ) (acc,1) cl))),i+1
+          (((name,UriManager.string_of_uri (UriManager.uri_of_uriref uri i
+          (Some j))) :: acc) , j+1)
+        ) (acc,1) cl)),i+1
   ) ([],0) types)
 
 let env_of_list l env =
- let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri suri) l in
+ let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri (UriManager.uri_of_string suri)) l in
   DisambiguateTypes.env_of_list l' env
 
 let add_aliases_for_inductive_def status types suri =