X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnUriManager.mli;h=911a1849b614a5b99c4f450f7b2cf9d8081675ae;hb=d9373d1ab9c84de43f212e11912178cabd5562ac;hp=b05ae502ceeda60cee40bfc0d460b26153187a6b;hpb=a3ba13b9503a2c0dd89b89b489899362d17b3f3a;p=helm.git diff --git a/helm/software/components/ng_kernel/nUriManager.mli b/helm/software/components/ng_kernel/nUriManager.mli index b05ae502c..911a1849b 100644 --- a/helm/software/components/ng_kernel/nUriManager.mli +++ b/helm/software/components/ng_kernel/nUriManager.mli @@ -23,12 +23,20 @@ * http://cs.unibo.it/helm/. *) -exception IllFormedUri of string Lazy.t;; +type spec = + | Decl + | Def + | Fix of int * int (* fixno, recparamno *) + | CoFix of int + | Ind of int + | IConstr of int * int (* indtyno, constrno *) -(* order, uri, (type, constructor) *) -type uri = private Uri of int * string * (int * int option ) option +type uri = Uri of int * string * spec val eq: uri -> uri -> bool - val string_of_uri: uri -> string + +(* CACCA *) +val nuri_of_ouri: UriManager.uri -> (int * int option ) option -> uri +val ouri_of_nuri: uri -> UriManager.uri