From 908672c4eb9bba99c43e8bb2a7376656429af6d7 Mon Sep 17 00:00:00 2001
From: mohring
Date: Wed, 6 Dec 2000 08:50:51 +0000
Subject: 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
---
 library/lib.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/lib.ml b/library/lib.ml
index 45877aa389..df48bc7cbd 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 ()
-- 
cgit v1.2.3