1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
(library
(name micromega_core_plugin)
(public_name rocq-runtime.plugins.micromega_core)
(modules micromega numCompat mutils sos_types sos_lib sos)
(synopsis "Rocq's micromega core plugin")
(libraries zarith rocq-runtime.clib))
(deprecated_library_name
(old_public_name coq-core.plugins.micromega_core)
(new_public_name rocq-runtime.plugins.micromega_core))
(library
(name micromega_plugin)
(public_name rocq-runtime.plugins.micromega)
; be careful not to link the executable to the plugin!
(modules (:standard \ micromega numCompat mutils sos_types sos_lib sos csdpcert g_zify zify))
(flags :standard -open Micromega_core_plugin)
(synopsis "Rocq's micromega plugin")
(libraries rocq-runtime.plugins.ltac rocq-runtime.plugins.micromega_core))
(deprecated_library_name
(old_public_name coq-core.plugins.micromega)
(new_public_name rocq-runtime.plugins.micromega))
(executable
(name csdpcert)
(public_name csdpcert)
(package rocq-runtime)
(modules csdpcert)
(flags :standard -open Micromega_core_plugin)
(libraries rocq-runtime.plugins.micromega_core))
(library
(name zify_plugin)
(public_name rocq-runtime.plugins.zify)
(modules g_zify zify)
(synopsis "Rocq's zify plugin")
(libraries rocq-runtime.plugins.ltac))
(deprecated_library_name
(old_public_name coq-core.plugins.zify)
(new_public_name rocq-runtime.plugins.zify))
(rule
(targets g_micromega.ml)
(deps (:mlg g_micromega.mlg))
(action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
(rule
(targets g_zify.ml)
(deps (:mlg g_zify.mlg))
(action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
|
