Fix a bug of Mltop.declare_cache_object.

Objects registered through the callback functions were pushed on the libstack
before the ML-MODULE object itself, leading to anomalies when the corresponding
object was assuming that the ML module was properly defined in any other Coq
module requiring the Declare ML command.

1 files changed, 8 insertions, 3 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 7218950da..f680ecee3 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -231,11 +231,16 @@ let add_leaves id objs =
   List.iter add_obj objs;
   oname
 
-let add_anonymous_leaf obj =
+let add_anonymous_leaf ?(cache_first = true) obj =
   let id = anonymous_id () in
   let oname = make_oname id in
-  cache_object (oname,obj);
-  add_entry oname (Leaf obj)
+  if cache_first then begin
+    cache_object (oname,obj);
+    add_entry oname (Leaf obj)
+  end else begin
+    add_entry oname (Leaf obj);
+    cache_object (oname,obj)
+  end
 
 let add_frozen_state () =
   add_anonymous_entry