diff options
| author | Pierre-Marie Pédrot | 2017-07-26 17:53:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-26 18:40:15 +0200 |
| commit | 4395637a6471fc95934fe93da671bda68d415a77 (patch) | |
| tree | fd51fbf117afb8dda9f97e1988e437c133ffeaa7 /tests | |
| parent | 2a74da7b6f275634fd8ed9c209edc73f2ae15427 (diff) | |
Ensuring that inductive constructors are always capitalized.
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. |