diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-01-23 17:32:58 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-05-23 10:48:28 +0200 |
commit | 352c23666babc7dd8f0136b02d9ef1893f9bde5c (patch) | |
tree | 10176ebba25fe2044c538c987674c84786d153ca /test-suite/coq-makefile/compat-subdirs | |
parent | 4252789c77479b9d4a9ac5a12e9a24067b086040 (diff) |
test suite for coq_makefile2
Diffstat (limited to 'test-suite/coq-makefile/compat-subdirs')
8 files changed, 3 insertions, 28 deletions
diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject index 700d59d64..4f44bde22 100644 --- a/test-suite/coq-makefile/compat-subdirs/_CoqProject +++ b/test-suite/coq-makefile/compat-subdirs/_CoqProject @@ -1,5 +1,5 @@ --R src/ test --R theories/ test +-R src test +-R theories test -I src src/test_plugin.mlpack diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh index 38e54d03e..ccb348c6f 100755 --- a/test-suite/coq-makefile/compat-subdirs/run.sh +++ b/test-suite/coq-makefile/compat-subdirs/run.sh @@ -3,8 +3,7 @@ #set -x set -e -export PATH=../../../bin/:$PATH -git clean -dfx . +. ../template/init.sh coq_makefile -f _CoqProject -o Makefile make exec test -f "subdir/done" diff --git a/test-suite/coq-makefile/compat-subdirs/src/test.ml4 b/test-suite/coq-makefile/compat-subdirs/src/test.ml4 deleted file mode 100644 index 8ddc9b095..000000000 --- a/test-suite/coq-makefile/compat-subdirs/src/test.ml4 +++ /dev/null @@ -1,13 +0,0 @@ -DECLARE PLUGIN "test_plugin" -let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; - -VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "Test" ] -> [ () ] -END - -TACTIC EXTEND test -| [ "test" ] -> [ Test_aux.tac ] -END - - - diff --git a/test-suite/coq-makefile/compat-subdirs/src/test.mli b/test-suite/coq-makefile/compat-subdirs/src/test.mli deleted file mode 100644 index e69de29bb..000000000 --- a/test-suite/coq-makefile/compat-subdirs/src/test.mli +++ /dev/null diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml b/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml deleted file mode 100644 index a01d0865a..000000000 --- a/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -let tac = Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli b/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli deleted file mode 100644 index 10020f27d..000000000 --- a/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -val tac : unit Proofview.tactic diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack b/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack deleted file mode 100644 index cf94d851b..000000000 --- a/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Test_aux -Test diff --git a/test-suite/coq-makefile/compat-subdirs/theories/test.v b/test-suite/coq-makefile/compat-subdirs/theories/test.v deleted file mode 100644 index 7753b56aa..000000000 --- a/test-suite/coq-makefile/compat-subdirs/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -Declare ML Module "test_plugin". -Test. -Goal True. -Proof. -test. -exact I. -Qed. |