(library
 (name nsatz_core_plugin)
 (public_name rocq-runtime.plugins.nsatz_core)
 (synopsis "Rocq's nsatz solver plugin")
 (modules (:standard \ g_nsatz))
 (libraries rocq-runtime.tactics))

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

(library
 (name nsatz_plugin)
 (public_name rocq-runtime.plugins.nsatz)
 (synopsis "Rocq's nsatz solver plugin (Ltac1 syntax)")
 (modules g_nsatz)
 (flags :standard -open Nsatz_core_plugin)
 (libraries rocq-runtime.plugins.nsatz_core rocq-runtime.plugins.ltac))

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

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