Reparation conditions de positivites inductifs, echange dans add_entry

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1057 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 3 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 45877aa38..df48bc7cb 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -84,13 +84,14 @@ let add_anonymous_entry node =
 
 let add_leaf id kind obj =
   let sp = make_path id kind in
-  add_entry sp (Leaf obj);
   cache_object (sp,obj);
+  add_entry sp (Leaf obj);
   sp
 
 let add_anonymous_leaf obj =
-  let sp = add_anonymous_entry (Leaf obj) in
-  cache_object (sp,obj)
+  let sp = make_path (anonymous_id()) OBJ in
+  cache_object (sp,obj);
+  add_entry sp (Leaf obj)
 
 let add_frozen_state () =
   let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in ()