Quelle  dune   Sprache: unbekannt

(library
 (name ltac_plugin)
 (public_name rocq-runtime.plugins.ltac)
 (synopsis "Rocq's LTAC tactic language")
 (modules :standard \ tauto)
 (modules_without_implementation tacexpr)
 (libraries rocq-runtime.vernac))

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

(library
 (name tauto_plugin)
 (public_name rocq-runtime.plugins.tauto)
 (synopsis "Rocq's tauto tactic")
 (modules tauto)
 (libraries rocq-runtime.plugins.ltac))

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

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

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

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

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

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

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

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

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

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

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

quality100%

[ Dauer der Verarbeitung: 0.19 Sekunden  (vorverarbeitet)  ]