diff options
| author | coq | 2006-02-15 17:06:13 +0000 |
|---|---|---|
| committer | coq | 2006-02-15 17:06:13 +0000 |
| commit | c3c28f6362f0489e680e8db75f34f7197755fba8 (patch) | |
| tree | d3f0fa761aa56bad9e5eaa38cd1c27b76d0114a5 /kernel | |
| parent | 9b252347567037dd48fcb7aff1e98bb83a11485f (diff) | |
continuing the generalization of "induction". Now induction schemes
with multiple args AND no main induction arg can be used directly with
induction. The last functional argument is not necessary anymore. For
example:
nat_double_ind:
forall R : nat -> nat -> Prop,
...branches...
-> forall n m : nat, R n m.
is ok.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8046 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions