Skip to content

Commit cfd4784

Browse files
committed
Updated g_coq_cw.ml4
1 parent 9d1f6b7 commit cfd4784

File tree

3 files changed

+28
-23
lines changed

3 files changed

+28
-23
lines changed

.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
*.d
66
/Makefile
77
Makefile.conf
8+
g_coq_cw.ml
89
.merlin
910
*.vo
1011
*.glob

_CoqProject

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,5 @@ theories/Loader.v
55

66
src/coq_cw.ml
77
src/coq_cw.mli
8-
src/g_coq_cw.ml4
8+
src/g_coq_cw.mlg
99
src/coq_cw_plugin.mlpack
Lines changed: 26 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -1,69 +1,73 @@
11
DECLARE PLUGIN "coq_cw_plugin"
22

3+
{
4+
35
open Stdarg
46

7+
}
8+
59
VERNAC COMMAND EXTEND CWAssertType CLASSIFIED AS QUERY
6-
| [ "CWAssert" string_opt(msg) ref(r) ":" constr(ty)] -> [
10+
| [ "CWAssert" string_opt(msg) ref(r) ":" constr(ty)] -> {
711
Coq_cw.test_type ?msg r ty
8-
]
12+
}
913
END
1014

1115
VERNAC COMMAND EXTEND CWAssertAssumptions CLASSIFIED AS QUERY
12-
| [ "CWAssert" string_opt(msg) ref(e) "Assumes" ref_list(axioms)] -> [
16+
| [ "CWAssert" string_opt(msg) ref(e) "Assumes" ref_list(axioms)] -> {
1317
Coq_cw.test_axioms ?msg e axioms
14-
]
18+
}
1519
END
1620

1721
VERNAC COMMAND EXTEND CWStopOnFailure CLASSIFIED AS SIDEFF
18-
| [ "CWStopOnFailure" int(flag)] -> [
22+
| [ "CWStopOnFailure" int(flag)] -> {
1923
Coq_cw.stop_on_failure flag
20-
]
24+
}
2125
END
2226

2327
VERNAC COMMAND EXTEND CWGroup CLASSIFIED AS SIDEFF
24-
| [ "CWGroup" string(msg)] -> [
28+
| [ "CWGroup" string(msg)] -> {
2529
Coq_cw.begin_group "DESCRIBE" msg
26-
]
30+
}
2731
END
2832

2933
VERNAC COMMAND EXTEND CWEndGroup CLASSIFIED AS SIDEFF
30-
| [ "CWEndGroup"] -> [
34+
| [ "CWEndGroup"] -> {
3135
Coq_cw.end_group "DESCRIBE"
32-
]
36+
}
3337
END
3438

3539
VERNAC COMMAND EXTEND CWTest CLASSIFIED AS SIDEFF
36-
| [ "CWTest" string(msg)] -> [
40+
| [ "CWTest" string(msg)] -> {
3741
Coq_cw.begin_group "IT" msg
38-
]
42+
}
3943
END
4044

4145
VERNAC COMMAND EXTEND CWEndTest CLASSIFIED AS SIDEFF
42-
| [ "CWEndTest"] -> [
46+
| [ "CWEndTest"] -> {
4347
Coq_cw.end_group "IT"
44-
]
48+
}
4549
END
4650

4751
VERNAC COMMAND EXTEND CWFileSize CLASSIFIED AS QUERY
48-
| [ "CWFile" string_opt(fname) "Size" "<" int(size)] -> [
52+
| [ "CWFile" string_opt(fname) "Size" "<" int(size)] -> {
4953
Coq_cw.test_file_size ?fname size
50-
]
54+
}
5155
END
5256

5357
VERNAC COMMAND EXTEND CWFileMatch CLASSIFIED AS QUERY
54-
| [ "CWFile" string_opt(fname) "Matches" string(regex)] -> [
58+
| [ "CWFile" string_opt(fname) "Matches" string(regex)] -> {
5559
Coq_cw.test_file_regex ?fname true regex
56-
]
60+
}
5761
END
5862

5963
VERNAC COMMAND EXTEND CWFileNegMatch CLASSIFIED AS QUERY
60-
| [ "CWFile" string_opt(fname) "Does" "Not" "Match" string(regex)] -> [
64+
| [ "CWFile" string_opt(fname) "Does" "Not" "Match" string(regex)] -> {
6165
Coq_cw.test_file_regex ?fname false regex
62-
]
66+
}
6367
END
6468

6569
VERNAC COMMAND EXTEND CWCompileAndRun CLASSIFIED AS SIDEFF
66-
| [ "CWCompileAndRun" string_list(files) "Options" string_opt(options) "Driver" string(driver) ] -> [
70+
| [ "CWCompileAndRun" string_list(files) "Options" string_opt(options) "Driver" string(driver) ] -> {
6771
Coq_cw.compile_and_run files ?options driver
68-
]
72+
}
6973
END

0 commit comments

Comments
 (0)