diff options
| author | letouzey | 2009-02-03 09:43:13 +0000 |
|---|---|---|
| committer | letouzey | 2009-02-03 09:43:13 +0000 |
| commit | aaf82265aca43a22006e6cf80f1b3cbe1fd594aa (patch) | |
| tree | 78809c61995d9da37828fa09ac8b063fd158b1c3 /toplevel | |
| parent | af188f7c62ae3cca7620f3738a264c70d2c56597 (diff) | |
Allow to turn contrib/subtac into a (nat)dynlink'able plugin
Main issue was declare_summary being triggered too late in
subtac_obligations, hence the associated init_function was
_not_ being done by Lib.init(). Fixed for the moment by
an ad-hoc launch of this init_function in subtac_obligations.
In other plugins, this issue doesn't appear, since
init_function is mostly putting back some empty set into
a reference that was initially empty. No need to really
run init_function in this case. For future plugins, we will
nonetheless have to be careful about that.
Of course, the (ref Obj.magic) was not exactly helpful in
debugging this matter, see http://caml.inria.fr/mantis/view.php?id=4707
As said by Xavier, naughty naughty boys...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11877 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/mltop.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index d1910c1452..9bac42c93c 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -231,7 +231,7 @@ let stdlib_use_plugins = Coq_config.has_natdynlink let initial_plugins = [ "Extraction_plugin"; "Cc_plugin"; "Ground_plugin"; "Dp_plugin"; - "Recdef_plugin"; (*"subtac_plugin";*) "Xml_plugin"; ] + "Recdef_plugin"; "Subtac_plugin"; "Xml_plugin"; ] (** Other plugins of the standard library. We need their list to avoid trying to load them if they have been statically compiled |