diff options
| author | Pierre-Marie Pédrot | 2017-08-01 00:35:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-01 00:35:09 +0200 |
| commit | 9eb7f16fc890a1bf3a1332332ed349513905ed66 (patch) | |
| tree | 5be5a85e5113d2036ff8c959d66746c55aeaf3ea /tests/example2.v | |
| parent | f9e7c43b5884f5231f14ec7b008b1eb660026a0e (diff) | |
Do not thunk notations preemptively.
One has to rely on the 'thunk' token to produce such thunks.
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 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. |