(library (name extraction_plugin) (public_name rocq-runtime.plugins.extraction) (synopsis "Rocq's extraction plugin") (libraries rocq-runtime.vernac)) (rule (targets g_extraction.ml) (deps (:mlg g_extraction.mlg)) (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))