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 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'library/lib.ml') 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 -- cgit v1.2.3