diff options
| author | Pierre-Marie Pédrot | 2017-08-08 14:21:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-08 15:26:11 +0200 |
| commit | 3fbba861d5355cad92cac52965c8e76a35825c7a (patch) | |
| tree | 4d90154704a17a98f822552711fe78c8fe24adb6 /tests | |
| parent | 3d1092cf7df3229ecc2a4da60a33cf7c6b9be1a3 (diff) | |
Another batch of primitive operations.
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/tacticals.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/tests/tacticals.v b/tests/tacticals.v new file mode 100644 index 0000000000..73f9c03b87 --- /dev/null +++ b/tests/tacticals.v @@ -0,0 +1,22 @@ +Require Import Ltac2.Ltac2. + +Import Ltac2.Notations. + +Goal True. +Proof. +Fail fail. +Fail solve [ () ]. +try fail. +repeat fail. +repeat (). +solve [ constructor ]. +Qed. + +Goal True. +Proof. +first [ + Message.print (Message.of_string "Yay"); fail +| constructor +| Message.print (Message.of_string "I won't be printed") +]. +Qed. |