-(* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *)
-
-exception OnlyPutOfInductiveDefinitionsIsAllowed
+(* get_cooked_obj_with_univlist ~trust uri *)
+(* returns the object if it is already type-checked or if it can be *)
+(* trusted (if [trust] = true and the trusting function accepts it) *)
+(* Otherwise it raises Not_found *)
+val get_cooked_obj_with_univlist :
+ ?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->
+ Cic.obj * CicUniv.universe_graph * CicUniv.universe list