+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 ->
+ 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 ->
+ bool * int * NCic.inductiveType list * NCic.i_attr * int
+
+val get_checked_fix:
+ NReference.reference ->
+ NCic.relevance * string * NCic.term * NCic.term * NCic.f_attr * int
+
+val get_checked_cofix:
+ NReference.reference ->
+ NCic.relevance * string * NCic.term * NCic.term * NCic.f_attr * int
+
+val get_indty_leftno: NReference.reference -> int