From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 7 Apr 2008 15:00:23 +0000 (+0000)
Subject: call get_obj instead of get_cooked_obj ~trust:false
X-Git-Tag: make_still_working~5425
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a84550090e4326ffacc08e423fbe00a590d446e3;p=helm.git

call get_obj instead of get_cooked_obj ~trust:false
---

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index c78508238..fcb408326 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -6,7 +6,9 @@ let get_checked_obj u =
   with Not_found ->
     let ouri = NUri.ouri_of_nuri u in
     let o,_ = 
-      CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph ouri 
+      try 
+        CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri 
+      with exn -> prerr_endline (UriManager.string_of_uri ouri); raise exn
     in
     (* FIX: add all objects to the environment and give back the last one *)
     let l = OCic2NCic.convert_obj ouri o in
@@ -22,7 +24,7 @@ let get_obj u =
     (* in th final implementation should get it from disk *)
     let ouri = NUri.ouri_of_nuri u in
     let o,_ = 
-      CicEnvironment.get_cooked_obj ~trust:true CicUniv.oblivion_ugraph ouri 
+      CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri 
     in
     let l = OCic2NCic.convert_obj ouri o in
     List.iter (fun (u,_,_,_,_ as o) ->