From: Stefano Zacchiroli <zack@upsilon.cc>
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)