From 6cfdf1ca60535f6e9ee6c5e0d5c546d34e803c61 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 5 Oct 2016 17:35:33 +0200
Subject: 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.
---
 library/lib.ml    | 11 ++++++++---
 library/lib.mli   |  2 +-
 toplevel/mltop.ml |  2 +-
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/library/lib.ml b/library/lib.ml
index 7218950da3..f680ecee3c 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 0a70152efb..a8e110c67a 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]
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 0a5b92270f..b6690fe47b 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -411,7 +411,7 @@ let inMLModule : ml_module_object -> obj =
 
 let declare_ml_modules local l =
   let l = List.map mod_of_name l in
-  Lib.add_anonymous_leaf (inMLModule {mlocal=local; mnames=l})
+  Lib.add_anonymous_leaf ~cache_first:false (inMLModule {mlocal=local; mnames=l})
 
 let print_ml_path () =
   let l = !coq_mlpath_copy in
-- 
cgit v1.2.3