Quelle  dune   Sprache: unbekannt

(library
 (name toplevel)
 (public_name rocq-runtime.toplevel)
 (synopsis "Rocq's Interactive Shell [terminal-based]")
 (wrapped false)
 ; until ocaml/dune#4892 fixed
 ; (private_modules g_toplevel)
 (libraries rocq-runtime.stm
  (select memtrace_init.ml from
   (memtrace -> memtrace_init.memtrace.ml)
   (!memtrace -> memtrace_init.default.ml))))

(deprecated_library_name
 (old_public_name coq-core.toplevel)
 (new_public_name rocq-runtime.toplevel))

; Interp provides the `zarith` library to plugins, we could also use
; -linkall in the plugins file, to be discussed.

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