added add_obj to store objects in the environment, implementation still

shaky since no frozen list is there

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 79014def5ef29866317569197dba712875688276..ff54e0232fb48a89885e19604f9f905faa466cb1 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -21,9 +21,15 @@ let get_obj u =
     let o,_ = 
       CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph ouri 
     in
+    (* here we should freeze it *)
     false, HExtlib.list_last (OCic2NCic.convert_obj ouri o)
 ;;
 
+let add_obj (u,_,_,_,_ as o) =
+  (* we should unfreeze it *)
+  NUri.UriHash.add cache u o
+;;
+
 let get_checked_def = function
   | NReference.Ref (_, uri, NReference.Def) ->
       (match get_checked_obj uri with

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 0984ea23f94e3a606121ced1ec669e2118517384..70a230ddf383eed8401fc3e2cb57d615d05b5d30 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -28,6 +28,7 @@
 
 val get_checked_obj: NUri.uri -> NCic.obj
 val get_obj: NUri.uri -> bool * NCic.obj
+val add_obj: NCic.obj -> unit
 
 val get_checked_def:
   NReference.reference ->