]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicUniv.mli
added orrible hack to make the current uri visible in the parser so that named univer...
[helm.git] / helm / ocaml / cic / cicUniv.mli
index 7bd224946afd02b181d58d38cbef232dc1d31d69..74af1ccc41114fd942eeb45c6ad54f88dc0a19e9 100644 (file)
@@ -43,7 +43,9 @@ type universe_graph
   returns a fresh universe
 *)
 val fresh: 
-  unit -> universe
+  ?uri:UriManager.uri ->
+  unit -> 
+    universe
 
 (*
   really useful at the begin and in all the functions that don't care