]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/urimanager/uriManager.ml
Merge of the V7_3_new_exportation branch.
[helm.git] / helm / ocaml / urimanager / uriManager.ml
index f45e65bf30e921e3605bbf3f415e0bc8536c6010..df707c956f2ba8f5e9de95d46480cf75d7cefdf9 100644 (file)
@@ -141,3 +141,20 @@ let annuri_of_uri uri =
 let uri_is_annuri uri =
  Str.string_match (Str.regexp ".*\.ann$") (string_of_uri uri) 0
 ;;
+
+let bodyuri_of_uri uri =
+ let struri = string_of_uri uri in
+  if Str.string_match (Str.regexp ".*\.con$") (string_of_uri uri) 0 then
+   let newuri = Array.copy uri in
+    newuri.(Array.length uri - 2) <- struri ^ ".body" ;
+    Some newuri
+  else
+   None
+;;
+
+let innertypesuri_of_uri uri =
+ let cicuri = cicuri_of_uri uri in
+  let newuri = Array.copy cicuri in
+   newuri.(Array.length cicuri - 2) <- (string_of_uri cicuri) ^ ".types" ;
+   newuri
+;;