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 | |
| parent | cfb181899cdd076fb7f2e061089ba76067e47ccc (diff) | |
Adding a file for testing typing.
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | tests/Makefile | 7 | ||||
| -rw-r--r-- | tests/stuff/ltac2.v (renamed from tests/ltac2.v) | 0 | ||||
| -rw-r--r-- | tests/typing.v | 25 |
4 files changed, 36 insertions, 0 deletions
@@ -10,3 +10,7 @@ clean: Makefile.coq Makefile.coq: _CoqProject $(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all 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 diff --git a/tests/ltac2.v b/tests/stuff/ltac2.v index 770d385406..770d385406 100644 --- a/tests/ltac2.v +++ b/tests/stuff/ltac2.v diff --git a/tests/typing.v b/tests/typing.v new file mode 100644 index 0000000000..8460ab42b7 --- /dev/null +++ b/tests/typing.v @@ -0,0 +1,25 @@ +Require Import Ltac2.Ltac2. + +(** Ltac2 is typed à la ML. *) + +Ltac2 test0 n := Int.add n 1. + +Print Ltac2 test0. + +Ltac2 test1 () := test0 0. + +Print Ltac2 test1. + +Fail Ltac2 test2 () := test0 true. + +Fail Ltac2 test2 () := test0 0 0. + +(** Polymorphism *) + +Ltac2 rec list_length l := +match l with +| [] => 0 +| x :: l => Int.add 1 (list_length l) +end. + +Print Ltac2 list_length. |