-(* set_cooking_function cooking_function *)
-val set_cooking_function :
- (Cic.obj -> UriManager.uri -> (int * Cic.obj) list) -> unit
+(* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *)
+
+exception OnlyPutOfInductiveDefinitionsIsAllowed
+
+(* put_inductive_definition uri obj *)
+(* put [obj] (that must be an InductiveDefinition and show URI is [uri]) *)
+(* in the environment. *)
+(* WARNING: VERY UNSAFE. *)
+(* This function should be called only on a well-typed definition. *)
+val put_inductive_definition : UriManager.uri -> Cic.obj -> unit