diff options
| author | Pierre-Marie Pédrot | 2017-07-26 16:38:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-26 17:28:46 +0200 |
| commit | 2a74da7b6f275634fd8ed9c209edc73f2ae15427 (patch) | |
| tree | cf120c751315f2e5f70bc8fc10209f962cf7d370 /tests/Makefile | |
| parent | cfb181899cdd076fb7f2e061089ba76067e47ccc (diff) | |
Adding a file for testing typing.
Diffstat (limited to 'tests/Makefile')
| -rw-r--r-- | tests/Makefile | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tests/Makefile b/tests/Makefile new file mode 100644 index 0000000000..a48ab0860f --- /dev/null +++ b/tests/Makefile @@ -0,0 +1,7 @@ +all: $(patsubst %.v,%.v.log,$(wildcard *.v)) + +%.v.log: %.v + $(COQBIN)/coqtop -I ../src -Q ../theories Ltac2 < $< 2> $@ + +clean: + rm -f *.log |