put_inductive_definition implemented and exposed.

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.mli

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index fbc53955ba80483c15311d4206cb144fe8e367d3..e93db958210ef5fa820d502f4317d2567f868a6c 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -61,8 +61,19 @@ val is_type_checked : ?trust:bool -> UriManager.uri -> type_checked_obj
 (* again in the future (is_type_checked will return true)             *)
 val set_type_checking_info : UriManager.uri -> unit
 
-(* get_cooked_obj ~trust uri *)
+(* get_cooked_obj ~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 : ?trust:bool -> UriManager.uri -> Cic.obj
+
+(* 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