aboutsummaryrefslogtreecommitdiff
path: root/plugins/btauto/btauto_plugin.mllib
AgeCommit message (Collapse)Author
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey
For now, the pack name reuse the previous .cma name of the plugin, (extraction_plugin, etc). The earlier .mllib files in plugins are now named .mlpack. They are also handled by bin/ocamllibdep, just as .mllib. We've slightly modified ocamllibdep to help setting the -for-pack options: in *.mlpack.d files, there are some extra variables such as foo/bar_FORPACK := -for-pack Baz when foo/bar.ml is mentioned in baz.mlpack. When a plugin is calling a function from another plugin, the name need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz). Btw, we discard the generated files plugins/*/*_mod.ml, they are obsolete now, replaced by DECLARE PLUGIN. Nota: there's a potential problem in the micromega directory, some .ml files are linked both in micromega_plugin and in csdpcert. And we now compile these files with a -for-pack, even if they are not packed in the case of csdpcert. In practice, csdpcert seems to work well, but we should verify with OCaml experts.
2012-01-13Added a Btauto plugin, that solves boolean tautologies.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14897 85f007b7-540e-0410-9357-904b9bb8a0f7