diff options
| author | emakarov | 2007-11-22 14:34:44 +0000 |
|---|---|---|
| committer | emakarov | 2007-11-22 14:34:44 +0000 |
| commit | 63e792e2cf320544bcd8b28b2e932b18d5f4af1f (patch) | |
| tree | c49f6ca226880dfa42d0f8160619219ebdb164a9 /theories/Numbers/Natural/Abstract/NBase.v | |
| parent | 20c0fdbc7f63b8c8ccaa0dd34e7d8105b94e804c (diff) | |
An update on Numbers. Added two files dealing with recursion, for information only.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10330 85f007b7-540e-0410-9357-904b9bb8a0f7
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 956eca896c..0a3d1a586e 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). |