X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Furimanager%2FuriManager.mli;h=703b0b4f1629e12639d64767a2c825b274fb49c8;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=8afb4e345ac28ee3d29ed6ecad88ff1af97eaf33;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli index 8afb4e345..703b0b4f1 100644 --- a/helm/ocaml/urimanager/uriManager.mli +++ b/helm/ocaml/urimanager/uriManager.mli @@ -36,11 +36,6 @@ val name_of_uri : uri -> string (* name only (without extension)*) val buri_of_uri : uri -> string (* base uri only *) val depth_of_uri : uri -> int (* length of the path *) -(* relative_depth curi uri cookingsno *) -(* is the number of times to cook uri to use it when the current uri is curi *) -(* cooked cookingsno times *) -val relative_depth : uri -> uri -> int -> int - (* given an uri, returns the uri of the corresponding cic file, *) (* i.e. removes the [.types][.ann] suffix *) val cicuri_of_uri : uri -> uri @@ -58,3 +53,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 +