diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/example2.v | 2 | ||||
| -rw-r--r-- | tests/stuff/ltac2.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tests/example2.v b/tests/example2.v index 14a6b68e18..5efbf90b34 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 ()). +Ltac2 Notation "split" bnd(bindings) := Std.split bnd. Goal exists n, n = 0. Proof. diff --git a/tests/stuff/ltac2.v b/tests/stuff/ltac2.v index 35546ef6c1..ece6fca06a 100644 --- a/tests/stuff/ltac2.v +++ b/tests/stuff/ltac2.v @@ -111,7 +111,7 @@ Proof. Fail zero (Bar "lol"). Abort. -Ltac2 Notation "refine!" c(constr) := refine c. +Ltac2 Notation "refine!" c(thunk(constr)) := refine c. Goal True. Proof. |