diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-05 17:35:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-05 17:53:59 +0200 |
| commit | 6cfdf1ca60535f6e9ee6c5e0d5c546d34e803c61 (patch) | |
| tree | abf69741eabceca7f824943cc864915ac014a0e8 | |
| parent | e2c0b6711ab100c1dc4d103601a951688b115c7c (diff) | |
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.
| -rw-r--r-- | library/lib.ml | 11 | ||||
| -rw-r--r-- | library/lib.mli | 2 | ||||
| -rw-r--r-- | toplevel/mltop.ml | 2 |
3 files changed, 10 insertions, 5 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] diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 0a5b92270..b6690fe47 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 |