aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-01 12:03:35 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-08 14:41:55 +0200
commit509c30c93dca8ca8c78f1da1eefc056226d90346 (patch)
tree9cc58803b234a38efd0cda5ca70b5105e08dd8d6 /plugins/funind
parentd060577f274658dd8189fceb92316b3cd37417b9 (diff)
Compilation via pack for plugins of the stdlib
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.
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/funind/recdef_plugin.mlpack (renamed from plugins/funind/recdef_plugin.mllib)1
2 files changed, 1 insertions, 2 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 80866e8b8..95b4967fa 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1529,7 +1529,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let hook _ _ =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
- let _ = Table.extraction_inline true [Ident (Loc.ghost,term_id)] in
+ let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.ghost,term_id)] in
(* message "start second proof"; *)
let stop =
try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mlpack
index ec1f5436c..2b443f2a1 100644
--- a/plugins/funind/recdef_plugin.mllib
+++ b/plugins/funind/recdef_plugin.mlpack
@@ -8,4 +8,3 @@ Invfun
Indfun
Merge
G_indfun
-Recdef_plugin_mod