diff options
| author | coq | 2006-02-10 18:34:51 +0000 |
|---|---|---|
| committer | coq | 2006-02-10 18:34:51 +0000 |
| commit | 94d27c5f40b55b06142443e8ae0b28c4432c090e (patch) | |
| tree | bf4196b721d9854cc203b6b96214a236e5b81b3c /kernel/type_errors.mli | |
| parent | 5384ed9ab7557c515c8522b0229f10663e5a3161 (diff) | |
induction now admits multiple induction arguments. The principle must
be explicitely given, and ALL parameters and args of the scheme must
be given (only branches must be omitted). For the moment, only
principle like generated by GenFixpoint (functional induction) are
usable. That is the predicate must have a additional paramter like in:
(P x1 ... xn (f p1...pm x1...xn))
Example of use : induction x y (add x y) using add_ind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8023 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions