From: Enrico Tassi Date: Fri, 1 Jul 2005 14:37:39 +0000 (+0000) Subject: added uri_is_ind X-Git-Tag: PRE_GETTER_STORAGE~60 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5e6e4586c8d8bd1707a38c5f24427fcfb1065d05;p=helm.git added uri_is_ind --- diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml index 296701af5..1ca99d972 100644 --- a/helm/ocaml/urimanager/uriManager.ml +++ b/helm/ocaml/urimanager/uriManager.ml @@ -86,6 +86,7 @@ let _dotann = ".ann" let _var = "var",3 let _dotbody = ".body" let _con = "con",3 +let _ind = "ind",3 let _xpointer = "#xpointer(1/" let _con3 = "con" let _var3 = "var" @@ -167,6 +168,8 @@ let uri_is_var (uri, _) = has_suffix uri _var let uri_is_con (uri, _) = has_suffix uri _con +let uri_is_ind (uri, _) = has_suffix uri _ind + let bodyuri_of_uri (uri, _) = if has_suffix uri _con then Some (uri_of_string (uri ^ _dotbody)) diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli index 86cd5c142..8691600a9 100644 --- a/helm/ocaml/urimanager/uriManager.mli +++ b/helm/ocaml/urimanager/uriManager.mli @@ -49,6 +49,7 @@ val annuri_of_uri : uri -> uri val uri_is_annuri : uri -> bool val uri_is_var : uri -> bool val uri_is_con : uri -> bool +val uri_is_ind : 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 *)