From f75b0191e4f4538ab5bfc47157438ac45bd26f16 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 15 Jul 2011 15:00:40 +0000 Subject: [PATCH] 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. --- matita/components/ng_kernel/nCicEnvironment.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 = -- 2.39.2