]> 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 53e6a6ffe5ecf54d72b62adfea1c2a97b409da9c..6f224d5273920710bfc14d47be5994878fa79065 100644 (file)
@@ -27,6 +27,8 @@
  * functions strictly necessary to the typechecking algorithm *)
 
 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 -> 
@@ -47,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 *)