X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;h=74e28ff9c7925c81bcb0ed0cdf7e5f01601e5209;hb=e28ddccd4096c80b2090ca78af00e2590f629b71;hp=c7389f16761b4d64579a9a3afb013378b3f790e7;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/ng_kernel/nCicEnvironment.ml b/matita/components/ng_kernel/nCicEnvironment.ml
index c7389f167..74e28ff9c 100644
--- a/matita/components/ng_kernel/nCicEnvironment.ml
+++ b/matita/components/ng_kernel/nCicEnvironment.ml
@@ -331,12 +331,14 @@ let check_and_add_obj (status:#NCic.status) ((u,_,_,_,_) as obj) =
   | e ->
      frozen_list := saved_frozen_list;
      let exn = `Exn e in
-     NUri.UriHash.add cache u exn;
      history := (`Obj (u,obj))::!history;
      if saved_frozen_list = [] then
       exn
      else
-      raise (Propagate (u,e))
+      begin
+       NUri.UriHash.add cache u exn;
+       raise (Propagate (u,e))
+      end
 ;;
 
 let get_checked_obj status u =