From ac0495a94c379731f40968b2e08d8f167f72ed64 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 19 Nov 2002 13:51:01 +0000 Subject: [PATCH] innertypesuri_of_uri implemented --- helm/ocaml/urimanager/uriManager.ml | 7 +++++++ helm/ocaml/urimanager/uriManager.mli | 3 +++ 2 files changed, 10 insertions(+) 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 -- 2.39.2