diff options
Diffstat (limited to 'tests/example2.v')
| -rw-r--r-- | tests/example2.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v index 6b26b78022..95485305dc 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -2,6 +2,8 @@ Require Import Ltac2.Ltac2. Import Ltac2.Notations. +Set Default Goal Selector "all". + Goal exists n, n = 0. Proof. split with (x := 0). |