put_inductive_definition implemented and exposed.

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

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index e9050cd8c1867ac6f0686abc2094facedfabcd9f..823aa3a40880b8500f6723fad1a8bfc76361ecff 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -61,6 +61,7 @@ module Cache :
    val frozen_to_cooked :
     uri:UriManager.uri -> unit
    val find_cooked : key:UriManager.uri -> Cic.obj
+   val add_cooked : key:UriManager.uri -> Cic.obj -> unit
   end 
 =
   struct
@@ -130,6 +131,7 @@ module Cache :
      Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
    ;;
    let find_cooked ~key:uri = CacheOfCookedObjects.find uri;;
+   let add_cooked ~key:uri obj = CacheOfCookedObjects.add uri obj;;
   end
 ;;
 
@@ -225,3 +227,11 @@ let get_obj uri =
   Not_found ->
    find_or_add_unchecked_to_cache uri
 ;; 
+
+exception OnlyPutOfInductiveDefinitionsIsAllowed
+
+let put_inductive_definition uri obj =
+ match obj with
+    Cic.InductiveDefinition _ -> Cache.add_cooked uri obj
+  | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed
+;;