diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZBase.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index e6eabd5b2c..d4f70adbc5 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -83,7 +83,7 @@ Tactic Notation "nzinduct" ident(n) := induction_maker n ltac:(apply bi_induction). Tactic Notation "nzinduct" ident(n) constr(u) := - induction_maker n ltac:(apply central_induction with (z := u)). + induction_maker n ltac:(apply (fun A A_wd => central_induction A A_wd u)). End NZBaseProp. |