(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}))))
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
*© Formatika GbR, Deutschland
