innertypesuri_of_uri implemented

diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml
index 9f969fdd12e11d699d53f11cb09f3029fa7bc59c..df707c956f2ba8f5e9de95d46480cf75d7cefdf9 100644 (file)
--- a/helm/ocaml/urimanager/uriManager.ml
+++ b/helm/ocaml/urimanager/uriManager.ml
@@ -151,3 +151,10 @@ let bodyuri_of_uri uri =
   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
+;;

diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli
index 5d6ad67831af0abc31c75f4c671d9ffffb24cb81..8afb4e345ac28ee3d29ed6ecad88ff1af97eaf33 100644 (file)
--- a/helm/ocaml/urimanager/uriManager.mli
+++ b/helm/ocaml/urimanager/uriManager.mli
@@ -55,3 +55,6 @@ val uri_is_annuri : uri -> bool
 (* given an uri of a constant, it gives back the uri of its body             *)
 (* it gives back None if the uri refers to a Variable or MutualInductiveType *)
 val bodyuri_of_uri : uri -> uri option
+
+(* given an uri, it gives back the uri of its inner types             *)
+val innertypesuri_of_uri : uri -> uri