diff options
| author | Pierre-Marie Pédrot | 2018-10-19 16:21:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-19 16:24:46 +0200 |
| commit | 266050f7aaa0ee0b090b30b1acabaccda6919889 (patch) | |
| tree | 290d511d83edbdd9709ccd2ec32c0ec05904c6ce /test-suite/coq-makefile | |
| parent | 3f6eebb9cfeda531d1f71e2ea0fa2d5afa9c28fc (diff) | |
Porting the test-suite to coqpp.
Diffstat (limited to 'test-suite/coq-makefile')
24 files changed, 29 insertions, 25 deletions
diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject index 53dc963997..ed31a58247 100644 --- a/test-suite/coq-makefile/arg/_CoqProject +++ b/test-suite/coq-makefile/arg/_CoqProject @@ -4,7 +4,7 @@ -arg "-w default" src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject index 4f44bde22a..1f914a71b0 100644 --- a/test-suite/coq-makefile/compat-subdirs/_CoqProject +++ b/test-suite/coq-makefile/compat-subdirs/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/coqdoc1/_CoqProject b/test-suite/coq-makefile/coqdoc1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/coqdoc1/_CoqProject +++ b/test-suite/coq-makefile/coqdoc1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/coqdoc2/_CoqProject b/test-suite/coq-makefile/coqdoc2/_CoqProject index d2a547d47b..0068554d72 100644 --- a/test-suite/coq-makefile/coqdoc2/_CoqProject +++ b/test-suite/coq-makefile/coqdoc2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject b/test-suite/coq-makefile/emptyprefix/_CoqProject index 5678a8edbb..3133342f6c 100644 --- a/test-suite/coq-makefile/emptyprefix/_CoqProject +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject @@ -4,7 +4,7 @@ -arg "-w default" src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/extend-subdirs/_CoqProject b/test-suite/coq-makefile/extend-subdirs/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/extend-subdirs/_CoqProject +++ b/test-suite/coq-makefile/extend-subdirs/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/findlib-package/_CoqProject +++ b/test-suite/coq-makefile/findlib-package/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/latex1/_CoqProject b/test-suite/coq-makefile/latex1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/latex1/_CoqProject +++ b/test-suite/coq-makefile/latex1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/merlin1/_CoqProject b/test-suite/coq-makefile/merlin1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/merlin1/_CoqProject +++ b/test-suite/coq-makefile/merlin1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/mlpack1/_CoqProject b/test-suite/coq-makefile/mlpack1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/mlpack1/_CoqProject +++ b/test-suite/coq-makefile/mlpack1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/mlpack2/_CoqProject b/test-suite/coq-makefile/mlpack2/_CoqProject index 51864a87ae..3db54e0a0b 100644 --- a/test-suite/coq-makefile/mlpack2/_CoqProject +++ b/test-suite/coq-makefile/mlpack2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/multiroot/_CoqProject b/test-suite/coq-makefile/multiroot/_CoqProject index b384bb6d97..f53eef99a8 100644 --- a/test-suite/coq-makefile/multiroot/_CoqProject +++ b/test-suite/coq-makefile/multiroot/_CoqProject @@ -4,7 +4,7 @@ -I src/ ./src/test_plugin.mllib -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/native1/_CoqProject b/test-suite/coq-makefile/native1/_CoqProject index a6fa17348c..847b2c00a9 100644 --- a/test-suite/coq-makefile/native1/_CoqProject +++ b/test-suite/coq-makefile/native1/_CoqProject @@ -4,7 +4,7 @@ -arg -native-compiler src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/only/_CoqProject b/test-suite/coq-makefile/only/_CoqProject index 357384fddf..619a8fa459 100644 --- a/test-suite/coq-makefile/only/_CoqProject +++ b/test-suite/coq-makefile/only/_CoqProject @@ -3,7 +3,7 @@ -I src/ ./src/test_plugin.mlpack -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin1/_CoqProject b/test-suite/coq-makefile/plugin1/_CoqProject index 4eddc9d708..ab7876d868 100644 --- a/test-suite/coq-makefile/plugin1/_CoqProject +++ b/test-suite/coq-makefile/plugin1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mllib -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin2/_CoqProject b/test-suite/coq-makefile/plugin2/_CoqProject index 0bf1e07f25..94eed53130 100644 --- a/test-suite/coq-makefile/plugin2/_CoqProject +++ b/test-suite/coq-makefile/plugin2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mllib -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin3/_CoqProject b/test-suite/coq-makefile/plugin3/_CoqProject index 2028d49a8b..8e8a7ab074 100644 --- a/test-suite/coq-makefile/plugin3/_CoqProject +++ b/test-suite/coq-makefile/plugin3/_CoqProject @@ -3,7 +3,7 @@ -I src/ ./src/test_plugin.mllib -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/quick2vo/_CoqProject +++ b/test-suite/coq-makefile/quick2vo/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index 2e066d30d9..30be5e6456 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -11,7 +11,7 @@ mkdir -p theories/sub cp ../../template/theories/sub/testsub.v theories/sub cp ../../template/theories/test.v theories -cp ../../template/src/test.ml4 src +cp ../../template/src/test.mlg src cp ../../template/src/test_aux.mli src cp ../../template/src/test.mli src cp ../../template/src/test_plugin.mlpack src diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.mlg index 72765abe04..7a166f3b98 100644 --- a/test-suite/coq-makefile/template/src/test.ml4 +++ b/test-suite/coq-makefile/template/src/test.mlg @@ -1,13 +1,17 @@ +{ open Ltac_plugin +} DECLARE PLUGIN "test_plugin" +{ let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; +} VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "TestCommand" ] -> [ () ] + | [ "TestCommand" ] -> { () } END TACTIC EXTEND test -| [ "test_tactic" ] -> [ Test_aux.tac ] +| [ "test_tactic" ] -> { Test_aux.tac } END diff --git a/test-suite/coq-makefile/uninstall1/_CoqProject b/test-suite/coq-makefile/uninstall1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/uninstall1/_CoqProject +++ b/test-suite/coq-makefile/uninstall1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/uninstall2/_CoqProject b/test-suite/coq-makefile/uninstall2/_CoqProject index d2a547d47b..0068554d72 100644 --- a/test-suite/coq-makefile/uninstall2/_CoqProject +++ b/test-suite/coq-makefile/uninstall2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/validate1/_CoqProject b/test-suite/coq-makefile/validate1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/validate1/_CoqProject +++ b/test-suite/coq-makefile/validate1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/vio2vo/_CoqProject +++ b/test-suite/coq-makefile/vio2vo/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli |