From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 4 Apr 2008 10:26:50 +0000 (+0000)
Subject: added add_obj to store objects in the environment, implementation still
X-Git-Tag: make_still_working~5454
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=637f6a77c970679ae9da4468e50bf5a3a6bf2853;p=helm.git

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 79014def5..ff54e0232 100644
--- 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 0984ea23f..70a230ddf 100644
--- 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 ->