X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FhelmLibraryObjects.ml;h=defc33f6cc63e6eef9b18b7c40332f0008214775;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=6ebdf8e1fac2cd0c94c5ae35b5da5060bdcec88e;hpb=971efe27973909c5d7eb9c9f9e6268585407da54;p=helm.git diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml index 6ebdf8e1f..defc33f6c 100644 --- a/helm/ocaml/cic/helmLibraryObjects.ml +++ b/helm/ocaml/cic/helmLibraryObjects.ml @@ -24,31 +24,6 @@ let indconuri_of_uri uri = int_of_string (String.sub uri index_con (String.length uri - index_con))) -(* (* NO LONGER USED, see CicUtil.term_of_uri *) -let term_of_uri ?(subst = []) uri = - let s = UriManager.string_of_uri uri in - try - (* Constant *) - let len = String.length s in - let sub = String.sub s (len -4) 4 in - if sub = ".con" then - const ~subst uri - else if sub = ".var" then - var ~subst uri - else - (try - (* Inductive Type *) - let (uri, typeno) = indtyuri_of_uri s in - mutind ~subst uri typeno - with - | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ -> - (* Constructor of an Inductive Type *) - let (uri, typeno, consno) = indconuri_of_uri s in - mutconstruct ~subst uri typeno consno) - with - | Invalid_argument _ | Not_found -> raise (UriManager.IllFormedUri s) -*) - (** {2 Helm's objects shorthands} *) module Logic =