support for subst

diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml
index af781edc8fb8cd7ca8bd08fc997c3a1bdd4b818f..3d32065becf7992dc8350bfab052d913cb709fc8 100644 (file)
--- 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)