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/uninstall1 | |
| parent | 4252789c77479b9d4a9ac5a12e9a24067b086040 (diff) | |
test suite for coq_makefile2
Diffstat (limited to 'test-suite/coq-makefile/uninstall1')
9 files changed, 4 insertions, 29 deletions
diff --git a/test-suite/coq-makefile/uninstall1/_CoqProject b/test-suite/coq-makefile/uninstall1/_CoqProject index 706cf75cc..35792066b 100644 --- a/test-suite/coq-makefile/uninstall1/_CoqProject +++ b/test-suite/coq-makefile/uninstall1/_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/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh index a3bfe182b..d24176279 100755 --- a/test-suite/coq-makefile/uninstall1/run.sh +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -3,8 +3,8 @@ #set -x set -e -export PATH=../../../bin/:$PATH -git clean -dfx . +. ../template/init.sh + coq_makefile -f _CoqProject -o Makefile make make html mlihtml diff --git a/test-suite/coq-makefile/uninstall1/src/test.ml4 b/test-suite/coq-makefile/uninstall1/src/test.ml4 deleted file mode 100644 index 8ddc9b095..000000000 --- a/test-suite/coq-makefile/uninstall1/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/uninstall1/src/test.mli b/test-suite/coq-makefile/uninstall1/src/test.mli deleted file mode 100644 index e69de29bb..000000000 --- a/test-suite/coq-makefile/uninstall1/src/test.mli +++ /dev/null diff --git a/test-suite/coq-makefile/uninstall1/src/test_aux.ml b/test-suite/coq-makefile/uninstall1/src/test_aux.ml deleted file mode 100644 index a01d0865a..000000000 --- a/test-suite/coq-makefile/uninstall1/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -let tac = Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/uninstall1/src/test_aux.mli b/test-suite/coq-makefile/uninstall1/src/test_aux.mli deleted file mode 100644 index 10020f27d..000000000 --- a/test-suite/coq-makefile/uninstall1/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -val tac : unit Proofview.tactic diff --git a/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack b/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack deleted file mode 100644 index cf94d851b..000000000 --- a/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Test_aux -Test diff --git a/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v b/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v deleted file mode 100644 index 755fc343f..000000000 --- a/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v +++ /dev/null @@ -1 +0,0 @@ -Require Import test. diff --git a/test-suite/coq-makefile/uninstall1/theories/test.v b/test-suite/coq-makefile/uninstall1/theories/test.v deleted file mode 100644 index 7753b56aa..000000000 --- a/test-suite/coq-makefile/uninstall1/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -Declare ML Module "test_plugin". -Test. -Goal True. -Proof. -test. -exact I. -Qed. |