X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicEnvironment.mli;h=80fcd2b68e4f993c3e49adfe2fe6c7c115df7399;hb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;hp=8483b8a1f771c17be9651dbf83458064051b5115;hpb=a4a2345e2efaf4cc64aa4daf40e2bce05a400f12;p=helm.git diff --git a/matita/components/ng_kernel/nCicEnvironment.mli b/matita/components/ng_kernel/nCicEnvironment.mli index 8483b8a1f..80fcd2b68 100644 --- a/matita/components/ng_kernel/nCicEnvironment.mli +++ b/matita/components/ng_kernel/nCicEnvironment.mli @@ -16,25 +16,25 @@ exception ObjectNotFound of string Lazy.t;; exception BadDependency of string Lazy.t * exn;; exception AlreadyDefined of string Lazy.t;; -val set_get_obj: (NUri.uri -> NCic.obj) -> unit +val set_get_obj: (NCic.status -> NUri.uri -> NCic.obj) -> unit -val get_checked_obj: NUri.uri -> NCic.obj +val get_checked_obj: #NCic.status -> NUri.uri -> NCic.obj -val check_and_add_obj: NCic.obj -> unit +val check_and_add_obj: #NCic.status -> NCic.obj -> unit -val get_relevance: NReference.reference -> bool list +val get_relevance: #NCic.status -> NReference.reference -> bool list val get_checked_def: - NReference.reference -> + #NCic.status -> NReference.reference -> NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int (* the last integer is the index of the inductive type in the reference *) val get_checked_indtys: - NReference.reference -> + #NCic.status -> NReference.reference -> bool * int * NCic.inductiveType list * NCic.i_attr * int val get_checked_fixes_or_cofixes: - NReference.reference -> + #NCic.status -> NReference.reference -> NCic.inductiveFun list * NCic.f_attr * int val invalidate_item: @@ -43,7 +43,7 @@ val invalidate_item: val invalidate: unit -> unit -val set_typecheck_obj: (NCic.obj -> unit) -> unit +val set_typecheck_obj: (NCic.status -> NCic.obj -> unit) -> unit (* =========== universes ============= *)