diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NBase.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 956eca896..0a3d1a586 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -141,7 +141,7 @@ refer to bidirectional induction, which is not useful on natural numbers. Therefore, we define a new induction tactic for natural numbers. We do not have to call "Declare Left Step" and "Declare Right Step" commands again, since the data for stepl and stepr tactics is inherited -from N. *) +from NZ. *) Ltac induct n := induction_maker n ltac:(apply induction). |