| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/toplevel/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 696 B |
|
Quelle dune Sprache: SML |
|||||||||
|
(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.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28