]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicLibrary.mli
huge commit regarding universes:
[helm.git] / helm / software / components / ng_kernel / nCicLibrary.mli
index d89db9d7114ed5022c9aa87b852f7100300a56c1..6dc7dde437d52e1e41e22e42e0bff7ee522c470a 100644 (file)
@@ -30,7 +30,7 @@ class status :
 (* it also checks it and add it to the environment *)
 val add_obj: #status as 'status -> NCic.obj -> 'status
 val add_constraint: 
-  #status as 'status -> bool -> NCic.universe -> NCic.universe -> 'status
+  #status as 'status -> NCic.universe -> NCic.universe -> 'status
 val aliases_of: NUri.uri -> NReference.reference list
 val resolve: string -> NReference.reference list
 (* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *)