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/goptions.ml | |
| 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/goptions.ml')
0 files changed, 0 insertions, 0 deletions