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 /library/lib.mli | |
| 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.
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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] |