]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicEnvironment.mli
added mk_fix i j r that given an r of a fix generated another fix on i and j
[helm.git] / helm / software / components / ng_kernel / nCicEnvironment.mli
index 0984ea23f94e3a606121ced1ec669e2118517384..6f224d5273920710bfc14d47be5994878fa79065 100644 (file)
@@ -28,6 +28,7 @@
 
 val get_checked_obj: NUri.uri -> NCic.obj
 val get_obj: NUri.uri -> bool * NCic.obj
+val add_obj: NCic.obj -> unit
 
 val get_checked_def:
   NReference.reference -> 
@@ -48,4 +49,8 @@ val get_checked_cofix:
 
 val get_indty_leftno: NReference.reference -> int
 
+val invalidate: unit -> unit
+val load_graph: UriManager.uri -> unit
+val get_graph: unit -> CicUniv.universe_graph
+
 (* EOF *)