From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 19 Nov 2002 13:51:01 +0000 (+0000)
Subject: innertypesuri_of_uri implemented
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ac0495a94c379731f40968b2e08d8f167f72ed64;p=helm.git

innertypesuri_of_uri implemented
---

diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml
index 9f969fdd1..df707c956 100644
--- 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 5d6ad6783..8afb4e345 100644
--- 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