diff options
Diffstat (limited to 'tests/example2.v')
| -rw-r--r-- | tests/example2.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/example2.v b/tests/example2.v index ffdb723ffb..398f33561e 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -1,6 +1,6 @@ Require Import Ltac2.Ltac2. -Ltac2 Notation "split" bnd(bindings) := Std.split bnd. +Import Ltac2.Notations. Goal exists n, n = 0. Proof. |