Skip to content

Commit 2e599a0

Browse files
committed
Changed ocamlopt to ocamlc
1 parent 38499eb commit 2e599a0

File tree

3 files changed

+5
-5
lines changed

3 files changed

+5
-5
lines changed

README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -71,12 +71,12 @@ Run `make .merlin` to create the `.merlin` file.
7171

7272
- `CWCompileAndRun ocaml_files* Options options? Driver driver_string`
7373

74-
Compiles and runs given `ocaml_files` and the driver code `driver_string`. The compilation is performed with `ocamlopt` and with the provided `options`.
74+
Compiles and runs given `ocaml_files` and the driver code `driver_string`. The compilation is performed with `ocamlc` and with the provided `options`.
7575

7676
```coq
7777
Require Extraction.
7878
Extraction "out.ml" plus.
79-
CWCompileAndRun "out.mli" "out.ml" Options "-O3 -verbose" Driver "
79+
CWCompileAndRun "out.mli" "out.ml" Options "-I . -verbose" Driver "
8080
open Out
8181
let () = assert (add O (S O) = (S O))
8282
".

cw_example_extraction/SolutionTest.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ CWTest "Successful Extraction Test".
1414

1515
Extraction "factorial.ml" Solution.factorial.
1616

17-
CWCompileAndRun "factorial.mli" "factorial.ml" Options "-O3" Driver "
17+
CWCompileAndRun "factorial.mli" "factorial.ml" Options "-verbose" Driver "
1818
open Factorial
1919
let () =
2020
assert (factorial 3 = 6);
@@ -28,7 +28,7 @@ Extract Constant mult => "*".
2828

2929
Extraction "factorial.ml" Solution.factorial.
3030

31-
CWCompileAndRun "factorial.mli" "factorial.ml" Options "-O2" Driver "
31+
CWCompileAndRun "factorial.mli" "factorial.ml" Options "-verbose" Driver "
3232
open Factorial
3333
let () =
3434
assert (factorial 3 = 6);

src/coq_cw.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
open Pp
22

33
let solution_file = "/workspace/Solution.v"
4-
let ocaml_compiler = "ocamlopt"
4+
let ocaml_compiler = "ocamlc"
55
let driver_file = "driver.ml"
66

77
let format_msg =

0 commit comments

Comments
 (0)