coq tests in own directory

kframework · Feb 11, 2020 · 17dee94 · 17dee94
1 parent d318981
commit 17dee94
Show file tree

Hide file tree

Showing 5 changed files with 1 addition and 1 deletion.
diff --git a/prover/build b/prover/build
@@ -53,7 +53,7 @@ prover_coq  = prover('prover-coq',  '--main-module DRIVER-COQ  --syntax-module D
 # prover_kore.tests(inputs = glob('t/*.kore'), implicit_inputs = glob('t/definitions/*.kore'), flags = '-cCOMMANDLINE=.CommandLine')
 # prover_smt .tests(inputs = glob('t/*.smt2'), flags = '-cCOMMANDLINE=.CommandLine')
 
-prover_coq .tests(inputs = glob('t/*.v'), flags = '-cCOMMANDLINE=.CommandLine')
+prover_coq .tests(inputs = glob('t/coq-tests/*.v'), flags = '-cCOMMANDLINE=.CommandLine')
 
 def log_on_success(file, message):
     return proj.rule( 'log-to-success'

diff --git a/prover/t/Logic.v → prover/t/coq-tests/Logic.v b/prover/t/Logic.v → prover/t/coq-tests/Logic.v
diff --git a/prover/t/Logic.v.expected → prover/t/coq-tests/Logic.v.expected b/prover/t/Logic.v.expected → prover/t/coq-tests/Logic.v.expected
diff --git a/prover/t/nat_ind.v → prover/t/coq-tests/nat_ind.v b/prover/t/nat_ind.v → prover/t/coq-tests/nat_ind.v
diff --git a/prover/t/nat_ind.v.expected → prover/t/coq-tests/nat_ind.v.expected b/prover/t/nat_ind.v.expected → prover/t/coq-tests/nat_ind.v.expected