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 c7389f16761b4d64579a9a3afb013378b3f790e7..74e28ff9c7925c81bcb0ed0cdf7e5f01601e5209 100644 (file)
--- 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 =