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
|
DECLARE PLUGIN "coq-simple-io.plugin"
{
open Stdarg
open IOLib
let run_ast = mk_ref "SimpleIO.IO_Monad.IO.unsafe_run'"
(* Since Coq 8.20, called as [run c ~opaque_access]. Before Coq 8.20, called as [run c]. *)
let run c =
#if COQ_VERSION >= (8,20,0)
fun ~opaque_access ->
#else
let opaque_access = () in
#endif
let name = string_of_constr_expr c in
run ~plugin_name:"coq_simple_io" ~opaque_access ~name
(CAst.make @@ apply_constr run_ast [c])
let string_unopt = function
| None -> ""
| Some s -> s
}
VERNAC COMMAND EXTEND RunIO CLASSIFIED AS SIDEFF
|
#if COQ_VERSION >= (8,20,0)
![opaque_access]
#endif
["RunIO" constr(c)] -> {run c}
| ["RunIO" "Include" string(s)] -> { add_extra_dir s }
| ["RunIO" "Open" string(s)] -> { add_module_to_open s }
| ["RunIO" "Package" string(s)] -> { add_extra_pkg s }
| ["RunIO" "Builder" "Ocamlfind" string_opt(opts)] -> { set_builder (Ocamlfind (string_unopt opts)) }
| ["RunIO" "Builder" "Ocamlbuild" string_opt(opts)] -> { set_builder (Ocamlbuild (string_unopt opts))}
| ["RunIO" "Builder" "Dune" string(s) string_opt(opts)] -> { set_builder (Dune (s, string_unopt opts)) }
| ["RunIO" "Smart" "On"] -> { smart_mode := true }
| ["RunIO" "Smart" "Off"] -> { smart_mode := false }
| ["RunIO" "Reset"] -> { IOLib.reset () }
| ["RunIO" "IOMode" "Repl"] -> { io_mode := Repl }
| ["RunIO" "IOMode" "Forward"] -> { io_mode := Forward }
END
|
