-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 * CicUniv.universe_graph) -> unit
-