X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Furimanager%2FuriManager.mli;h=12775af8d48fd9a3168fbc149bfc7ebbf7ec4766;hb=cfff4940f12cd8f82c745e84403317b9eee964e7;hp=0f4f15ea2822ce998847a7312759a7352dfb397f;hpb=0d436761ba03acfadbfe913c0a38367068bdbb47;p=helm.git diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli index 0f4f15ea2..12775af8d 100644 --- a/helm/ocaml/urimanager/uriManager.mli +++ b/helm/ocaml/urimanager/uriManager.mli @@ -40,6 +40,8 @@ val depth_of_uri : uri -> int (* length of the path *) (* i.e. removes the [.types][.ann] suffix *) val cicuri_of_uri : uri -> uri +val strip_xpointer: uri -> uri (* remove trailing #xpointer..., if any *) + (* given an uri, returns the uri of the corresponding annotation file, *) (* i.e. adds the .ann suffix if not already present *) val annuri_of_uri : uri -> uri @@ -53,3 +55,15 @@ 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 + +(* +val mutind_uri: uri -> int -> uri +val mutconstruct_uri: uri -> int -> int -> uri +val mutind: uri -> uri * int +val mutconstruct: uri -> uri * int * int +*) + + (* builder for MutInd and MutConstruct URIs *) +type uriref = uri * (int list) +val string_of_uriref : uriref -> string +