From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Jul 2011 15:00:40 +0000 (+0000)
Subject: Bug fixed: when we try to add an object and it is not _directly_ well typed
X-Git-Tag: make_still_working~2366
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f75b0191e4f4538ab5bfc47157438ac45bd26f16;p=helm.git

Bug fixed: when we try to add an object and it is not _directly_ well typed
(i.e. it is not well typed, and not because it depends on a non-well-typed
object in the library), we should not remember it, since the user can change
the definition and try again.
---

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 =