From: Stefano Zacchiroli Date: Wed, 11 Feb 2004 12:02:46 +0000 (+0000) Subject: support for subst X-Git-Tag: V_0_3_0~19 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1337fb2d670d110d72f4c04e9d69852660e282ab;p=helm.git support for subst --- diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml index af781edc8..3d32065be 100644 --- a/helm/ocaml/cic/helmLibraryObjects.ml +++ b/helm/ocaml/cic/helmLibraryObjects.ml @@ -24,7 +24,7 @@ let indconuri_of_uri uri = int_of_string (String.sub uri index_con (String.length uri - index_con))) -let term_of_uri uri = +let term_of_uri ?(subst = []) uri = let s = UriManager.string_of_uri uri in try (* Constant *) @@ -32,19 +32,19 @@ let term_of_uri uri = let len = String.length s in let sub = String.sub s (len -4) 4 in if sub = ".con" then - const uri + const ~subst uri else if sub = ".var" then - var uri + var ~subst uri else (try (* Inductive Type *) let (uri, typeno) = indtyuri_of_uri s in - mutind uri typeno + 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 uri typeno consno) + mutconstruct ~subst uri typeno consno) with | Invalid_argument _ | Not_found -> raise (UriManager.IllFormedUri s)