aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/native
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2019-04-12 15:35:55 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2019-04-12 15:35:55 +0200
commit93bd71388291d2e526a30c56e7fe63744f98e64d (patch)
tree0204b122319ce802e06d8cc9722b597fc4b62c54 /src/versions/native
parentbcf5d896d5b8bf371f4873dcc86ec2d2f8734eeb (diff)
downloadsmtcoq-93bd71388291d2e526a30c56e7fe63744f98e64d.tar.gz
smtcoq-93bd71388291d2e526a30c56e7fe63744f98e64d.zip
Separate unit tests into vernac and tactics
Diffstat (limited to 'src/versions/native')
-rw-r--r--src/versions/native/Make7
-rw-r--r--src/versions/native/Makefile10
2 files changed, 6 insertions, 11 deletions
diff --git a/src/versions/native/Make b/src/versions/native/Make
index a9e60e4..f45eb72 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -37,10 +37,9 @@
-I versions/native
--custom "cd ../unit-tests; make" "" "test"
--custom "cd ../unit-tests; make zchaff" "" "ztest"
--custom "cd ../unit-tests; make verit" "" "vtest"
--custom "cd ../unit-tests; make lfsc" "" "lfsctest"
+-custom "cd ../unit-tests; make vernac" "" "test"
+-custom "cd ../unit-tests; make zchaffv" "" "ztest"
+-custom "cd ../unit-tests; make veritv" "" "vtest"
-custom "$(CAMLLEX) $<" "%.mll" "%.ml"
-custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
index 4683956..3c6bf30 100644
--- a/src/versions/native/Makefile
+++ b/src/versions/native/Makefile
@@ -339,17 +339,14 @@ ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/sm
%.ml: %.mll
$(CAMLLEX) $<
-lfsctest:
- cd ../unit-tests; make lfsc
-
vtest:
- cd ../unit-tests; make verit
+ cd ../unit-tests; make veritv
ztest:
- cd ../unit-tests; make zchaff
+ cd ../unit-tests; make zchaffv
test:
- cd ../unit-tests; make
+ cd ../unit-tests; make vernac
####################
# #
@@ -417,7 +414,6 @@ clean:
- rm -rf $(CMXS)
- rm -rf $(CMXA)
- rm -rf ml
- - rm -rf lfsctest
- rm -rf vtest
- rm -rf ztest
- rm -rf test