diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/stuff/ltac2.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/stuff/ltac2.v b/tests/stuff/ltac2.v index 770d385406..36ea1ef4c1 100644 --- a/tests/stuff/ltac2.v +++ b/tests/stuff/ltac2.v @@ -18,7 +18,7 @@ Ltac2 foo' _ := ident:(bla). Print Ltac2 foo'. -Ltac2 bar x H := match x with +Ltac2 bar x h := match x with | None => constr:(fun H => ltac2:(exact (hyp ident:(H))) -> nat) | Some x => x end. |