]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic/cicUniv.mli
Bug fixed: types were check for conversion in the wrong context.
[helm.git] / helm / software / components / cic / cicUniv.mli
index 7b422583f53f361da3e247fb5717ac313eb7f70c..6451a74ec619abf63c65bbc4a6a0c1efe16739ec 100644 (file)
@@ -133,6 +133,7 @@ val restart_numbering:
   returns the universe number (used to save it do xml) 
 *) 
 val univno: universe -> int 
+val univuri: universe -> UriManager.uri
 
   (** re-hash-cons URIs contained in the given universe so that phisicaly
    * equality could be enforced. Mainly used by