]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mQueryMisc.ml
moved string_of_uriref from MQueryMisc to UriManager
[helm.git] / helm / ocaml / mathql / mQueryMisc.ml
index fb32d8c2425fb49fbd59f254e855a7c790d2ccf7..08474d3947aac3b2d6220ab61edae443bebf8e14 100644 (file)
@@ -106,15 +106,3 @@ let term_of_cic_textual_parser_uri uri =
    | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
 ;;
 
-(* conversion functions *****************************************************)
-
-type uriref = UriManager.uri * (int list)
-
-let string_of_uriref (uri, fi) =
-   let module UM = UriManager in
-   let str = UM.string_of_uri uri in
-   let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in
-   match fi with
-      | []          -> str 
-      | [t]         -> str ^ xp t ^ ")" 
-      | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")"