changed type of ids_to_uris table to (Cic.id, UriManager.uri) Hashtbl.t

[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index ddf429db6d469f36a8d1542adf30ad63f0a1fcbc..b1892e64a1973fe767afb237c7285d931f5d1e95 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -36,7 +36,7 @@ type pretty_printer_id = pattern_id
 
 type term_info =
   { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
-    uri: (Cic.id, string) Hashtbl.t;
+    uri: (Cic.id, UriManager.uri) Hashtbl.t;
   }
 
 let get_types uri =
@@ -297,7 +297,7 @@ let ast_of_acic0 term_info acic k =
   let aux = function
     | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None))
     | Cic.AVar (id,uri,substs) ->
-        register_uri id (UriManager.string_of_uri uri);
+        register_uri id uri;
         idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))
     | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l))
     | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
@@ -322,19 +322,19 @@ let ast_of_acic0 term_info acic k =
           k s, k t))
     | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args))
     | Cic.AConst (id,uri,substs) ->
-        register_uri id (UriManager.string_of_uri uri);
+        register_uri id uri;
         idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))
     | Cic.AMutInd (id,uri,i,substs) as t ->
         let name = name_of_inductive_type uri i in
         let uri_str = UriManager.string_of_uri uri in
         let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (i+1) in
-        register_uri id puri_str;
+        register_uri id (UriManager.uri_of_string puri_str);
         idref id (Ast.Ident (name, aux_substs substs))
     | Cic.AMutConstruct (id,uri,i,j,substs) ->
         let name = constructor_of_inductive_type uri i j in
         let uri_str = UriManager.string_of_uri uri in
         let puri_str = sprintf "%s#xpointer(1/%d/%d)" uri_str (i + 1) j in
-        register_uri id puri_str;
+        register_uri id (UriManager.uri_of_string puri_str);
         idref id (Ast.Ident (name, aux_substs substs))
     | Cic.AMutCase (id,uri,typeno,ty,te,patterns) ->
         let name = name_of_inductive_type uri typeno in
@@ -578,8 +578,7 @@ let rec ast_of_acic1 term_info annterm =
             let idref = CicUtil.id_of_annterm annterm in
             (try
               register_uri idref
-                (UriManager.string_of_uri
-                  (CicUtil.uri_of_term (Deannotate.deannotate_term annterm)))
+                (CicUtil.uri_of_term (Deannotate.deannotate_term annterm))
             with Invalid_argument _ -> ());
             idref)
           ctors