(library
 (name micromega_core_plugin)
 (public_name rocq-runtime.plugins.micromega_core)
 (modules micromega numCompat mutils sos_types sos_lib sos)
 (synopsis "Rocq's micromega core plugin")
 (libraries zarith rocq-runtime.clib))

(deprecated_library_name
 (old_public_name coq-core.plugins.micromega_core)
 (new_public_name rocq-runtime.plugins.micromega_core))

(library
 (name micromega_plugin)
 (public_name rocq-runtime.plugins.micromega)
 ; be careful not to link the executable to the plugin!
 (modules (:standard \ micromega numCompat mutils sos_types sos_lib sos csdpcert g_zify zify))
 (flags :standard -open Micromega_core_plugin)
 (synopsis "Rocq's micromega plugin")
 (libraries rocq-runtime.plugins.ltac rocq-runtime.plugins.micromega_core))

(deprecated_library_name
 (old_public_name coq-core.plugins.micromega)
 (new_public_name rocq-runtime.plugins.micromega))

(executable
 (name csdpcert)
 (public_name csdpcert)
 (package rocq-runtime)
 (modules csdpcert)
 (flags :standard -open Micromega_core_plugin)
 (libraries rocq-runtime.plugins.micromega_core))

(library
 (name zify_plugin)
 (public_name rocq-runtime.plugins.zify)
 (modules g_zify zify)
 (synopsis "Rocq's zify plugin")
 (libraries rocq-runtime.plugins.ltac))

(deprecated_library_name
 (old_public_name coq-core.plugins.zify)
 (new_public_name rocq-runtime.plugins.zify))

(rule
 (targets g_micromega.ml)
 (deps (:mlg g_micromega.mlg))
 (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

(rule
 (targets g_zify.ml)
 (deps (:mlg g_zify.mlg))
 (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))