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.

2 files changed, 9 insertions, 4 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
diff --git a/library/lib.mli b/library/lib.mli
index 0a70152ef..a8e110c67 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -54,7 +54,7 @@ val segment_of_objects :
   current list of operations (most recent ones coming first). *)
 
 val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name
-val add_anonymous_leaf : Libobject.obj -> unit
+val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
 val pull_to_head : Libnames.object_name -> unit
 
 (** this operation adds all objects with the same name and calls [load_object]