diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-10 18:34:51 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-10 18:34:51 +0000 |
| commit | 94d27c5f40b55b06142443e8ae0b28c4432c090e (patch) | |
| tree | bf4196b721d9854cc203b6b96214a236e5b81b3c /proofs/clenvtac.ml | |
| 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 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 6a0ea6096..8bba76007 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -66,6 +66,7 @@ let clenv_refine clenv gls = (refine (clenv_cast_meta clenv (clenv_value clenv))) gls + let res_pf clenv ?(allow_K=false) gls = clenv_refine (clenv_unique_resolver allow_K clenv gls) gls |